Results from the last SVComp shows that JR has raised null pointer exception when running on apachicli_eqchk. This resulted in us producing unknown result.
the stack trace is below
`region summary single path optimization applied.
UnrecognizedOptionException: Unrecognized option:
at Parser.processOption(Parser.java:455)
at Parser.parse(Parser.java:208)
at Parser.parse(Parser.java:109)
at CLI.execute(CLI.java:75)
at CLI.mainProcess(CLI.java:65)
at Main.runCLI(Main.java:8)
at Main.testFunction(Main.java:21)
at TestCLI.JRWrapper(TestCLI.java:30)
at TestCLI.testHarness(TestCLI.java:18)
at TestCLI.runTest(TestCLI.java:34)
at Main.main(Main.java:16)
stateAdvanced
====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.NullPointerException: Calling 'equals(Ljava/lang/Object;)Z' on null object
at TestCLI.testHarness(TestCLI.java:19)
at TestCLI.runTest(TestCLI.java:34)
at Main.main(Main.java:16)
====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
call stack:
at TestCLI.testHarness(TestCLI.java:19)
at TestCLI.runTest(TestCLI.java:34)
at Main.main(Main.java:16)
/**** Printing Exception Statistics *****
Static Analysis exceptions count = 63
Instantiation Time exceptions count = 2255
Unknown phases exception count = 490
FindStructuredBlockEndNode: mal-formed region: (51, StaticAnalysisPhase)
cannot make ArrayRef for symbolic array reference: (1760, InstantiationPhase)
region contains condition that cannot be instantiated: (6, StaticAnalysisPhase)
createComplexIfCondition: unconditional branch (continue or break): (3, StaticAnalysisPhase)
trying to compose with two null statements: (490, Unknown phase)
out of bounds array access in ArrayExpressions: (490, InstantiationPhase)
region instantiation is not beneficial (2,2): (5, InstantiationPhase)
Untranslatable instruction in SSAToStatIVisitor: (3, StaticAnalysisPhase)
/**** Printing Time Decomposition Statistics *****
static analysis time = 1909 msec
Veritesting Dyn Time = 20516 msec
Veritesting fix-point Time = 0 msec
/**** Printing Solver Statistics *****
Total Solver Queries Count = 4209
Total Solver Time = 6767 msec
Total Solver Parse Time = 1054 msec
Region Summary Parse Time = 0 msec
Total Solver Clean up Time = 550 msec
PCSatSolverCount = 119
PCSatSolverTime = 2320 msec
Constant Propagation Time for PC sat. checks = 2
Array SPF Case count = 194
If-removed count = 200
/**** Printing Region Statistics *****
Number of Distinct Veritested Regions = 5
Number of Distinct Un-Veritested Symbolic Regions = 10
Number of Distinct Failed Regions for Field Reference = 0
Number of Distinct Failed Regions for SPFCases = 0
Number of Distinct Failed Regions for missing method summaries = 1
Number of Distinct Failed Regions for Other Reasons = 9
Number of High Order Regions Used = 0
/**** Printing Instantiation Statistics *****
Number of successful instantiations = 119
Total Number of unsuccessful instantiations = 496
Number of failed instantiations due to Field Reference = 0
Number of failed instantiations due to SPFCases = 0
Number of failed instantiations due to missing method summaries = 1
Number of failed instantiations due to Other Reasons = 495
Number of Veritested Regions Instances = 119
Printing keys of regions that were instantiated at least once
Options.shortOptsContain(C)Z#28
Options.shortOptsContain(C)Z#34
Options.shortOptsContain_get(C)Z#28
Options.shortOptsContain_get(C)Z#34
Parser.parse(LOptions;[[CLjava/util/Properties;Z)LCommandLine;#315
Finished printing keys of regions that were instantiated at least once
Results from the last SVComp shows that JR has raised null pointer exception when running on
apachicli_eqchk. This resulted in us producingunknownresult.the stack trace is below
`region summary single path optimization applied. UnrecognizedOptionException: Unrecognized option: at Parser.processOption(Parser.java:455) at Parser.parse(Parser.java:208) at Parser.parse(Parser.java:109) at CLI.execute(CLI.java:75) at CLI.mainProcess(CLI.java:65) at Main.runCLI(Main.java:8) at Main.testFunction(Main.java:21) at TestCLI.JRWrapper(TestCLI.java:30) at TestCLI.testHarness(TestCLI.java:18) at TestCLI.runTest(TestCLI.java:34) at Main.main(Main.java:16) stateAdvanced
====================================================== error 1 gov.nasa.jpf.vm.NoUncaughtExceptionsProperty java.lang.NullPointerException: Calling 'equals(Ljava/lang/Object;)Z' on null object at TestCLI.testHarness(TestCLI.java:19) at TestCLI.runTest(TestCLI.java:34) at Main.main(Main.java:16)
====================================================== snapshot #1 thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TestCLI.testHarness(TestCLI.java:19) at TestCLI.runTest(TestCLI.java:34) at Main.main(Main.java:16)
====================================================== VeritestingListener report:
/**** Printing Exception Statistics ***** Static Analysis exceptions count = 63 Instantiation Time exceptions count = 2255 Unknown phases exception count = 490 FindStructuredBlockEndNode: mal-formed region: (51, StaticAnalysisPhase) cannot make ArrayRef for symbolic array reference: (1760, InstantiationPhase) region contains condition that cannot be instantiated: (6, StaticAnalysisPhase) createComplexIfCondition: unconditional branch (continue or break): (3, StaticAnalysisPhase) trying to compose with two null statements: (490, Unknown phase) out of bounds array access in ArrayExpressions: (490, InstantiationPhase) region instantiation is not beneficial (2,2): (5, InstantiationPhase) Untranslatable instruction in SSAToStatIVisitor: (3, StaticAnalysisPhase)
/**** Printing Time Decomposition Statistics ***** static analysis time = 1909 msec Veritesting Dyn Time = 20516 msec Veritesting fix-point Time = 0 msec
/**** Printing Solver Statistics ***** Total Solver Queries Count = 4209 Total Solver Time = 6767 msec Total Solver Parse Time = 1054 msec Region Summary Parse Time = 0 msec Total Solver Clean up Time = 550 msec PCSatSolverCount = 119 PCSatSolverTime = 2320 msec Constant Propagation Time for PC sat. checks = 2 Array SPF Case count = 194 If-removed count = 200
/**** Printing Region Statistics ***** Number of Distinct Veritested Regions = 5 Number of Distinct Un-Veritested Symbolic Regions = 10 Number of Distinct Failed Regions for Field Reference = 0 Number of Distinct Failed Regions for SPFCases = 0 Number of Distinct Failed Regions for missing method summaries = 1 Number of Distinct Failed Regions for Other Reasons = 9 Number of High Order Regions Used = 0
/**** Printing Instantiation Statistics ***** Number of successful instantiations = 119 Total Number of unsuccessful instantiations = 496 Number of failed instantiations due to Field Reference = 0 Number of failed instantiations due to SPFCases = 0 Number of failed instantiations due to missing method summaries = 1 Number of failed instantiations due to Other Reasons = 495
Number of Veritested Regions Instances = 119 Printing keys of regions that were instantiated at least once Options.shortOptsContain(C)Z#28 Options.shortOptsContain(C)Z#34 Options.shortOptsContain_get(C)Z#28 Options.shortOptsContain_get(C)Z#34 Parser.parse(LOptions;[[CLjava/util/Properties;Z)LCommandLine;#315 Finished printing keys of regions that were instantiated at least once
Metrics Vector: 22425,1909,20516,151,4209,6767,1054,550,5,10,0,0,0,1,9,0,15,119,496,0,0,0,1,495,42364,17334,6,10,2.215384615384615,63,2255,490
====================================================== results error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.NullPointerException: Calling 'equals(Lj..."
====================================================== statistics elapsed time: 00:00:22 states: new=314,visited=0,backtracked=302,end=151 search: maxDepth=13,constraints=6 choice generators: thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=159 heap: new=69570,released=85542,maxLive=614,gcCycles=308 instructions: 3929002 max memory: 654MB loaded code: classes=102,methods=2123
====================================================== search finished: 11/30/19 5:11 AM UNKNOWN`