MergeRuleTests

11

tests

0

failures

0

ignored

1m37.74s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 15.817s passed
testDoAutomaticGcdProofWithMergePointStatements() 15.465s passed
testDoManualGcdProof() 27.426s passed
testLoadClosedGcdProofWithMergePointStatements() 5.863s passed
testLoadGcdProof() 5.441s passed
testLoadGcdProofWithPredAbstr() 5.989s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 5.320s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.471s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 4.018s passed
testMergeIndistinguishablePathConditionsWithITE() 4.096s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.830s passed

Standard output

605308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
605308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 489.9ns 
605308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605480     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
605480     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
605480     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
605480     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
606151     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
610592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.28s 
610670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
610670     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 
632731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
632731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.7ns 
632731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
636765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.03s 
636827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
637202     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 369.24ms 
637202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
637202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.6ns 
637218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.03s 
641299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
641315     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.4ns 
653019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
653019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 366.7ns 
653024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
657182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.17s 
657260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
658323     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03s 
658339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
658339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 507.6ns 
658339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
662576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.23s 
662639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
664312     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61s 
664328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
664328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 500.8ns 
664328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
668127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.79s 
668143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
668158     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
668158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
668174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 584.7ns 
668174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
672114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.95s 
672145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
672145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 906.3ns 
672176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
672176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.5ns 
672176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
676319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.14s 
676366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
678023     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6s 
678039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
678039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 847.5ns 
678054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
682104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.05s 
682135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
682135     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 884.3ns 
682135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
682135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 566.5ns 
682135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
685997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.86s 
686060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
686060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.3ns 
697600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
697600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 559.8ns 
697600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
701572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.97s 
701618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
703025     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35s