MergeRuleTests

11

tests

0

failures

0

ignored

1m26.17s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 14.130s passed
testDoAutomaticGcdProofWithMergePointStatements() 13.699s passed
testDoManualGcdProof() 24.683s passed
testLoadClosedGcdProofWithMergePointStatements() 5.216s passed
testLoadGcdProof() 4.447s passed
testLoadGcdProofWithPredAbstr() 4.468s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.855s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.777s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.360s passed
testMergeIndistinguishablePathConditionsWithITE() 3.238s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.298s passed

Standard output

509053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
509053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 350.9ns 
509053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509178     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
509178     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
509178     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
509178     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
509758     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
513627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.58s 
513674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
513674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 
533731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
533731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.4ns 
533731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
537226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
538508     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21s 
538523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
538523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 414ns 
538523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
541961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
541961     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.3ns 
552638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
552638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.6ns 
552638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
556109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
557493     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 755.57ms 
557493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
557493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.5ns 
557493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 
561067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
561961     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 853.04ms 
561961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
561961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.9ns 
561961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
565243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
565259     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 699.9ns 
565259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
565259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.1ns 
565259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
568537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
568583     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 971.4ns 
568619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
568619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 472.5ns 
568619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.96s 
572624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
573820     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09s 
573836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
573836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.23ms 
573836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
577074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
577074     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 504.1ns 
577074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
577074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.6ns 
577089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
580430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
580430     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.7ns 
590773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
590773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 424.2ns 
590788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 
594314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
595220     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 856.83ms