MergeRuleTests

11

tests

0

failures

0

ignored

1m46.53s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 17.492s passed
testDoAutomaticGcdProofWithMergePointStatements() 17.497s passed
testDoManualGcdProof() 29.873s passed
testLoadClosedGcdProofWithMergePointStatements() 6.613s passed
testLoadGcdProof() 5.675s passed
testLoadGcdProofWithPredAbstr() 7.646s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 5.034s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.581s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.925s passed
testMergeIndistinguishablePathConditionsWithITE() 4.252s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.940s passed

Standard output

610226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
610226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 504.7ns 
610226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610507     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
610507     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
610507     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
610507     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
611163     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
615603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.37s 
615651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
615666     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 
640101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
640101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 544.2ns 
640101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
644244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.14s 
644308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
644683     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 359.07ms 
644683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
644683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 335ns 
644683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.06s 
648825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
648841     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.4ns 
662175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
662175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.2ns 
662175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
666240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.05s 
666303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
667193     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 858.01ms 
667209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
667209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 620.1ns 
667209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
671322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.12s 
671384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
674839     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.06s 
674855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
674855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.3ns 
674855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
678748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.9s 
678780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
678795     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
678795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
678795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.8ns 
678795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
682564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.76s 
682658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
682658     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 418.8ns 
682720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
682720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.6ns 
682720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
686972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.25s 
687035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
689286     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.17s 
689333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
689333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.9ns 
689333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
693554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.21s 
693585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
693585     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 338.1ns 
693585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
693585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 415.5ns 
693585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
697525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.94s 
697588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
697603     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.9ns 
711082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
711082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 814.4ns 
711082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
715756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.67s 
715819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
716741     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 871.91ms