====================================================== search started: 18.12.14 11:07
ALOAD pcHeap: constraint # = 1
poor_1_SYMREF == CONST_-1
====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.NullPointerException: Calling 'getStatus()Lbank/Status;' on null object <--- correctly detects possible NPE
at bank.Bank.isRich(Bank.java:20)
at bank.SPFDriver.main(SPFDriver.java:23)
====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
call stack:
at bank.Bank.isRich(Bank.java:20)
at bank.SPFDriver.main(SPFDriver.java:23)
ALOAD pcHeap: constraint # = 1
poor_1_SYMREF[377] != CONST_-1
lazy initialization
# heap cg registered: gov.nasa.jpf.symbc.heap.HeapChoiceGenerator[id="?",isCascaded:false,0..1,delta=+1,cur=-1]
lazy initialization
GETFIELD pcHeap: constraint # = 2
poor_1_SYMREF[377]._status == CONST_-1 &&
poor_1_SYMREF[377] != CONST_-1
====================================================== error 2
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty <--- I don't understand this error, does JPF cannot resolve equals method ?
java.lang.NoSuchMethodError: ?UNKNOWN?.equals(Ljava/lang/Object;)Z
at bank.Bank.isRich(Bank.java:20)
at bank.SPFDriver.main(SPFDriver.java:23)
====================================================== snapshot #2
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
call stack:
at bank.Bank.isRich(Bank.java:20)
at bank.SPFDriver.main(SPFDriver.java:23)
lazy initialization
GETFIELD pcHeap: constraint # = 2
poor_1_SYMREF[377]._status[394] != CONST_-1 &&
poor_1_SYMREF[377] != CONST_-1
lazy initialization
lazy initialization
GETSTATIC pcHeap: constraint # = 3
bank.Status.RICH == poor_1_SYMREF[377]._status[394] &&
poor_1_SYMREF[377]._status[394] != CONST_-1 &&
poor_1_SYMREF[377] != CONST_-1
lazy initialization
GETSTATIC pcHeap: constraint # = 3
bank.Status.RICH == CONST_-1 &&
poor_1_SYMREF[377]._status[394] != CONST_-1 &&
poor_1_SYMREF[377] != CONST_-1
lazy initialization
GETSTATIC pcHeap: constraint # = 4
bank.Status.RICH[395] != poor_1_SYMREF[377]._status[394] &&
bank.Status.RICH[395] != CONST_-1 &&
poor_1_SYMREF[377]._status[394] != CONST_-1 &&
poor_1_SYMREF[377] != CONST_-1
====================================================== coverage statistics