| method | List getCertificateInfo(int) |
| pre | index >= 0 |
| pre | this.chain != null |
| pre | this.chain.length >= 1 |
| pre | index < this.chain.length |
| pre | (soft) this.chain[...] != null |
| pre | (soft) this.manager != null |
| presumption | com.dmdirc.CertificateManager:getDNFieldsFromCert(. ..)@134 != null |
| presumption | java.security.cert.X509Certificate:getNotAfter(... )@128 != null |
| presumption | java.security.cert.X509Certificate:getNotBefore(... )@126 != null |
| presumption | java.security.cert.X509Certificate:getSerialNumber( ...)@150 != null |
| post | return_value == &new ArrayList(getCertificateIn fo#1) |
| post | new ArrayList(getCertificateInfo#1) num objects == 1 |
| unanalyzed | call on java.lang.Throwable:__curr_excep_obj |
| unanalyzed | call on java.util.Map:get |
| unanalyzed | call on java.util.List:add |
| unanalyzed | call on java.security.cert.X509Certificate:getSubje ctAlternativeNames |
| unanalyzed | call on java.util.Collection:iterator |
| unanalyzed | call on java.util.List:get |
| unanalyzed | call on java.lang.Integer:intValue |
| unanalyzed | call on java.util.Map:containsKey |
| method | String getAlternateNames(X509Certificate) |
| pre | (soft) cert != null |
| presumption | java.security.cert.X509Certificate:getSubjectAltern ativeNames(...)@169 != null |
| presumption | java.util.Iterator:next(...)@169 != null |
| presumption | java.util.List:get(...)@170 != null |
| post | java.lang.StringBuilder:toString(...)._tainted == 0 |
| post | return_value in Addr_Set{null,&java.lang. StringBuilder:toString(...)} |
| test_vector | java.lang.Integer:intValue(...)@170: {-231..1, 3..6, 8..232-1}, {7} |
| test_vector | java.lang.StringBuilder:length(...)@174: {-231..0}, {1..232-1} |
| test_vector | java.security.cert.X509Certificate:getSubjectAltern ativeNames(...)@165: Inverse{null}, Addr_Set{null} |