Messages

Last Msg First Msg

method

com.dmdirc.util.ConfigFile__static_init

method	void com.dmdirc.util.ConfigFile(InputStream)
post	init'ed(this.charset)
post	this.domains == &new ArrayList(ConfigFile#1)
post	this.flatdomains == &new MapList(ConfigFile#2)
post	this.is == is
post	init'ed(this.is)
post	this.keydomains == &new HashMap(ConfigFile#3)
post	new ArrayList(ConfigFile#1) num objects == 1
post	new HashMap(ConfigFile#3) num objects == 1
post	new HashMap(MapList#1) num objects == 1
post	new MapList(ConfigFile#2) num objects == 1
post	this.flatdomains.map == &new HashMap(MapList#1)
unanalyzed	call on java.util.HashMap

method	void com.dmdirc.util.ConfigFile(File)
post	init'ed(this.charset)
post	this.domains == &new ArrayList(ConfigFile#1)
post	this.file == file
post	init'ed(this.file)
post	this.flatdomains == &new MapList(ConfigFile#2)
post	this.keydomains == &new HashMap(ConfigFile#3)
post	new ArrayList(ConfigFile#1) num objects == 1
post	new HashMap(ConfigFile#3) num objects == 1
post	new HashMap(MapList#1) num objects == 1
post	new MapList(ConfigFile#2) num objects == 1
post	this.flatdomains.map == &new HashMap(MapList#1)
unanalyzed	call on java.util.HashMap

method	void com.dmdirc.util.ConfigFile(String)
post	init'ed(this.charset)
post	this.domains == &new ArrayList(ConfigFile#1)
post	this.file == &new File(ConfigFile#1)
post	this.flatdomains == &new MapList(ConfigFile#2)
post	this.keydomains == &new HashMap(ConfigFile#3)
post	new ArrayList(ConfigFile#1) num objects == 1
post	new File(ConfigFile#1) num objects == 1
post	new HashMap(ConfigFile#3) num objects == 1
post	new HashMap(MapList#1) num objects == 1
post	new MapList(ConfigFile#2) num objects == 1
post	new MapList(ConfigFile#2).map == &new HashMap(MapList#1)
unanalyzed	call on java.nio.charset.Charset:forName
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.HashMap

method	void setAutomake(bool)
post	this.automake == automake
post	init'ed(this.automake)

method	void read()
pre	this.domains != null
pre	init'ed(this.file)
pre	this.flatdomains != null
pre	this.flatdomains.map != null
pre	this.keydomains != null
pre	(soft) init'ed(this.is)
presumption	java.util.Iterator:next(...)@112 != null
presumption	java.util.Map:get(...)@142 != null
post	this.lines == &new ArrayList(readLines#4)
post	new ArrayList(readLines#4) num objects == 1
post	new ArrayList(readLines#4) num objects == 0
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.Map:put
unanalyzed	call on java.util.Map:clear
unanalyzed	call on java.io.FileInputStream
unanalyzed	call on java.io.InputStreamReader
unanalyzed	call on java.io.BufferedReader
unanalyzed	call on java.io.BufferedReader:readLine
unanalyzed	call on java.util.List:add
unanalyzed	call on java.io.BufferedReader:close
unanalyzed	call on java.util.List:contains
unanalyzed	call on java.lang.Exception
test_vector	java.lang.String:charAt(...)@115: {9}, {0..8, 10..2¹⁶-1}
test_vector	java.lang.String:charAt(...)@115: {0..31, 33..2¹⁶-1}, {32}
test_vector	java.lang.String:endsWith(...)@122: {0}, {1}
test_vector	java.lang.String:endsWith(...)@122: {1}, {0}
test_vector	java.lang.String:indexOf(...)@120: {0}, {-2³¹..-1, 1..2³²-1}
test_vector	java.lang.String:isEmpty(...)@115: {1}, {0}
test_vector	java.lang.String:isEmpty(...)@120: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@112: {0}, {1}
test_vector	java.util.Map:containsKey(...)@132: {1}, {0}
test_vector	java.util.Map:containsKey(...)@84: {1}, {0}

Prev Msg Next Msg

conditional throw

click for all messages in this file Medium Prob.

check that domain != null

conditional throw

Low Prob.

check that keydomain == 0

Prev Msg Next Msg

method	void write()
pre	this.domains != null
pre	this.file != null
pre	(soft) this.flatdomains != null
pre	(soft) this.flatdomains.map != null
pre	(soft) this.keydomains != null
presumption	java.util.GregorianCalendar:getTime(...)@166 != null
presumption	java.util.Iterator:next(...)@170 != null
presumption	java.util.Iterator:next(...)@180 != null
presumption	java.util.Iterator:next(...)@184 != null
presumption	java.util.Map:entrySet(...)@184 != null
presumption	java.util.Map:get(...)@107 != null
presumption	java.util.Map:get(...)@184 != null
presumption	java.util.Map_Entry:getKey(...)@185 != null
presumption	java.util.Map_Entry:getValue(...)@185 != null
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.lang.String:replaceAll
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.io.FileWriter
unanalyzed	call on java.io.BufferedWriter
unanalyzed	call on java.io.BufferedWriter:write
unanalyzed	call on java.io.BufferedWriter:newLine
unanalyzed	call on java.io.BufferedWriter:close
test_vector	java.lang.String:equals(...)@171: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@170: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@184: {0}, {1}
test_vector	java.util.Map:containsKey(...)@84: {0}, {1}

method	void writeMeta(List)
pre	lines != null
pre	this.domains != null
pre	(soft) this.keydomains != null
test_vector	java.lang.String:equals(...)@207: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@206: {0}, {1}
test_vector	java.util.Map:containsKey(...)@209: {0}, {1}

method	Map getKeyDomains()
post	return_value == this.keydomains
post	init'ed(return_value)

method	Map getKeyDomain(String)
pre	init'ed(this.automake)
pre	this.keydomains != null
pre	(soft) this.domains != null
post	init'ed(return_value)
unanalyzed	call on java.util.Map:containsKey
test_vector	this.automake: {0}, {1}
test_vector	java.util.Map:containsKey(...)@267: {1}, {0}

method	List getFlatDomain(String)
pre	this.flatdomains != null
pre	this.flatdomains.map != null
post	init'ed(return_value)
unanalyzed	call on java.util.Map:get

method	bool hasDomain(String)
pre	this.keydomains != null
pre	(soft) this.flatdomains != null
pre	(soft) this.flatdomains.map != null
post	init'ed(return_value)
unanalyzed	call on java.util.Map:containsKey

method	bool isKeyDomain(String)
pre	this.keydomains != null
post	init'ed(return_value)

method	bool isFlatDomain(String)
pre	this.flatdomains != null
pre	this.flatdomains.map != null
post	init'ed(return_value)
unanalyzed	call on java.util.Map:containsKey

method	void addDomain(String, List)
pre	this.domains != null
pre	this.flatdomains != null
pre	this.flatdomains.map != null
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.Map:put
unanalyzed	call on java.util.List:addAll

method	void addDomain(String, Map)
pre	this.domains != null
pre	this.keydomains != null

method	String unescape(String)
pre	input != null
post	java.lang.StringBuilder:toString(...)._tainted == 0
post	return_value == &java.lang.StringBuilder:toStri ng(...)
test_vector	java.lang.String:charAt(...)@314: {110}, {92}, {114}

method	String escape(String)
pre	input != null
post	return_value != null

method	int findEquals(String)
pre	input != null
post	return_value in {-1..2³²-2}
test_vector	java.lang.String:charAt(...)@361: {0..91, 93..2¹⁶-1}, {92}
test_vector	java.lang.String:charAt(...)@363: {0..60, 62..2¹⁶-1}, {61}