CipherUtils.java

CipherUtils.java

current inspection = 2009-09-03 21:56:13 (id #1)

Filter Options

Annotation Kind:

pre

presumption

post

unanalyzed

test_vector

bool auth()

Kind	Annotation Text
pre	(soft) init'ed(this.password)
presumption	com.dmdirc.config.IdentityManager:getConfigIdentity (...)@242 != null
presumption	com.dmdirc.config.IdentityManager:getGlobalConfig(. ..)@229 != null
presumption	com.dmdirc.config.IdentityManager:getGlobalConfig(. ..)@230 != null
presumption	com.dmdirc.config.IdentityManager:getGlobalConfig(. ..)@232 != null
presumption	com.dmdirc.config.IdentityManager:getGlobalConfig(. ..)@234 != null
presumption	getUserInput(...)@266 != null
post	init'ed(return_value)
post	init'ed(this.password)
unanalyzed	call on com.dmdirc.Main:getUI
unanalyzed	call on com.dmdirc.logger.Logger:userError
unanalyzed	call on getUserInput
unanalyzed	call on java.lang.String
unanalyzed	call on java.lang.String:getBytes
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.nio.charset.Charset:forName
unanalyzed	call on java.security.MessageDigest:digest
unanalyzed	call on java.security.MessageDigest:getInstance
test_vector	com.dmdirc.config.ConfigManager:hasOptionString(... )@229: {0}, {1}
test_vector	com.dmdirc.config.ConfigManager:hasOptionString(... )@232: {0}, {1}
test_vector	java.lang.String:equals(...)@245: {1}, {0}
test_vector	java.lang.String:isEmpty(...)@238: {0}, {1}

bool checkAuthed()

Kind	Annotation Text
pre	(soft) init'ed(this.ecipher)
pre	init'ed(this.dcipher)
post	init'ed(return_value)
test_vector	this.dcipher: Addr_Set{null}, Inverse{null}
test_vector	this.ecipher: Addr_Set{null}, Inverse{null}

void com.dmdirc.util.CipherUtils()

Kind	Annotation Text
post	new byte[](CipherUtils#1) num objects == 1
post	this.SALT == &new byte[](CipherUtils#1)
post	this.SALT.length == 8
post	this.SALT[0] == -87
post	this.SALT[1] == -101
post	this.SALT[2] == -56
post	this.SALT[3] == 50
post	this.SALT[4] == 86
post	this.SALT[5] == 53
post	this.SALT[6] == -29
post	this.SALT[7] == 3

com.dmdirc.util.CipherUtils__static_init

Kind	Annotation Text

void createCiphers()

Kind	Annotation Text
pre	(soft) this.password != null
presumption	init'ed(com.dmdirc.logger.ErrorLevel.LOW)
presumption	javax.crypto.Cipher:getInstance(...)@191 != null
presumption	javax.crypto.Cipher:getInstance(...)@192 != null
presumption	javax.crypto.SecretKeyFactory:generateSecret(... )@189 != null
presumption	javax.crypto.SecretKeyFactory:getInstance(...)@189 != null
post	init'ed(this.dcipher)
post	init'ed(this.ecipher)

String decrypt(String)

Kind	Annotation Text
pre	(soft) init'ed(net.miginfocom.Base64__static_init. new int[](Base64__static_init#1)[...])
pre	(soft) init'ed(this.ecipher)
pre	(soft) init'ed(this.password)
pre	init'ed(this.dcipher)
presumption	init'ed(com.dmdirc.logger.ErrorLevel.LOW)
post	init'ed(this.dcipher)
post	init'ed(this.ecipher)
post	init'ed(this.password)
post	new String(decrypt#1) num objects <= 1
post	return_value in Addr_Set{null,&new String(decrypt#1)}
unanalyzed	call on com.dmdirc.Main:getUI
unanalyzed	call on com.dmdirc.config.ConfigManager:getOption
unanalyzed	call on com.dmdirc.config.ConfigManager:hasOptionSt ring
unanalyzed	call on com.dmdirc.config.Identity:setOption
unanalyzed	call on com.dmdirc.config.IdentityManager:getConfig Identity
unanalyzed	call on com.dmdirc.config.IdentityManager:getGlobal Config
unanalyzed	call on com.dmdirc.logger.Logger:userError
unanalyzed	call on getUserInput
unanalyzed	call on java.lang.String
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.String:getBytes
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.nio.charset.Charset:forName
unanalyzed	call on java.security.MessageDigest:digest
unanalyzed	call on java.security.MessageDigest:getInstance
unanalyzed	call on javax.crypto.Cipher:getInstance
unanalyzed	call on javax.crypto.Cipher:init
unanalyzed	call on javax.crypto.SecretKey:getAlgorithm
unanalyzed	call on javax.crypto.SecretKeyFactory:generateSecre t
unanalyzed	call on javax.crypto.SecretKeyFactory:getInstance
unanalyzed	call on javax.crypto.spec.PBEKeySpec
unanalyzed	call on javax.crypto.spec.PBEParameterSpec
test_vector	!(this.dcipher == null) & !(this.ecipher == null): {1}, {0}

String encrypt(String)

Kind	Annotation Text
pre	(soft) init'ed(this.ecipher)
pre	(soft) init'ed(this.password)
pre	(soft) str != null
pre	init'ed(this.dcipher)
presumption	init'ed(com.dmdirc.logger.ErrorLevel.LOW)
presumption	javax.crypto.Cipher:doFinal(...).length@117 in {0, 3..169_538_366}
post	init'ed(this.dcipher)
post	init'ed(this.ecipher)
post	init'ed(this.password)
post	new String(encodeToString#1) num objects <= 1
post	return_value in Addr_Set{null,&new String(encodeToString#1)}
unanalyzed	call on com.dmdirc.Main:getUI
unanalyzed	call on com.dmdirc.config.ConfigManager:getOption
unanalyzed	call on com.dmdirc.config.ConfigManager:hasOptionSt ring
unanalyzed	call on com.dmdirc.config.Identity:setOption
unanalyzed	call on com.dmdirc.config.IdentityManager:getConfig Identity
unanalyzed	call on com.dmdirc.config.IdentityManager:getGlobal Config
unanalyzed	call on com.dmdirc.logger.Logger:userError
unanalyzed	call on getUserInput
unanalyzed	call on java.lang.String
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.String:getBytes
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.nio.charset.Charset:forName
unanalyzed	call on java.security.MessageDigest:digest
unanalyzed	call on java.security.MessageDigest:getInstance
unanalyzed	call on javax.crypto.Cipher:getInstance
unanalyzed	call on javax.crypto.Cipher:init
unanalyzed	call on javax.crypto.SecretKey:getAlgorithm
unanalyzed	call on javax.crypto.SecretKeyFactory:generateSecre t
unanalyzed	call on javax.crypto.SecretKeyFactory:getInstance
unanalyzed	call on javax.crypto.spec.PBEKeySpec
unanalyzed	call on javax.crypto.spec.PBEParameterSpec
test_vector	!(this.dcipher == null) & !(this.ecipher == null): {1}, {0}

CipherUtils getCipherUtils()

Kind	Annotation Text
pre	init'ed(me)
post	me != null
post	me == One-of{old me, &new CipherUtils(getCipher Utils#1)}
post	new CipherUtils(getCipherUtils#1) num objects <= 1
post	new CipherUtils(getCipherUtils#1).SALT == &new byte[](CipherUtils#1)
post	new byte[](CipherUtils#1) num objects <= 1
post	new byte[](CipherUtils#1).length == 8
post	new byte[](CipherUtils#1)[0] == -87
post	new byte[](CipherUtils#1)[1] == -101
post	new byte[](CipherUtils#1)[2] == -56
post	new byte[](CipherUtils#1)[3] == 50
post	new byte[](CipherUtils#1)[4] == 86
post	new byte[](CipherUtils#1)[5] == 53
post	new byte[](CipherUtils#1)[6] == -29
post	new byte[](CipherUtils#1)[7] == 3
post	return_value != null
post	return_value == One-of{old me, &new CipherUtils(getCipherUtils#1)}
test_vector	me: Inverse{null}, Addr_Set{null}

String getPassword(String)

Kind	Annotation Text
presumption	com.dmdirc.Main:getUI(...)@266 != null
post	init'ed(return_value)

String hash(String)

Kind	Annotation Text
pre	(soft) data != null
presumption	init'ed(com.dmdirc.logger.ErrorLevel.LOW)
presumption	java.security.MessageDigest:getInstance(...)@160 != null
post	new String(hash#1) num objects <= 1
post	return_value in Addr_Set{null,&new String(hash#1)}