MergeRuleTests

11

tests

0

failures

0

ignored

1m31.54s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 16.135s passed
testDoAutomaticGcdProofWithMergePointStatements() 14.745s passed
testDoManualGcdProof() 24.991s passed
testLoadClosedGcdProofWithMergePointStatements() 5.425s passed
testLoadGcdProof() 4.863s passed
testLoadGcdProofWithPredAbstr() 5.379s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 5.067s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.237s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.519s passed
testMergeIndistinguishablePathConditionsWithITE() 3.564s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.611s passed

Standard output

555914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
555914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 424.3ns 
555929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556070     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
556070     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
556070     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
556070     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
556852     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
560463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.53s 
560510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
560510     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 
580931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
580931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.1ns 
580931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.76s 
584762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
585153     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 377.17ms 
585153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
585153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 264.3ns 
585153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.92s 
589155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
589155     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.7ns 
601304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
601304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187ns 
601304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.9s 
605261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
606340     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04s 
606355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
606355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.9ns 
606355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.86s 
610264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
611734     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41s 
611734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
611734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 440ns 
611749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.58s 
615345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
615345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
615345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
615345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.4ns 
615361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 
618832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
618832     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 951.5ns 
618864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
618864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.5ns 
618864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.65s 
622569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
624273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65s 
624289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
624304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.92ms 
624304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 
627853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
627853     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 947ns 
627853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
627853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.1ns 
627853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
631261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
631261     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.5ns 
642598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
642598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.5ns 
642598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
646163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.56s 
646210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
647461     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2s