MergeRuleTests

11

tests

0

failures

0

ignored

1m29.29s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 14.792s passed
testDoAutomaticGcdProofWithMergePointStatements() 14.760s passed
testDoManualGcdProof() 25.965s passed
testLoadClosedGcdProofWithMergePointStatements() 4.999s passed
testLoadGcdProof() 4.811s passed
testLoadGcdProofWithPredAbstr() 5.041s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.495s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.817s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.446s passed
testMergeIndistinguishablePathConditionsWithITE() 3.552s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.615s passed

Standard output

534968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
534968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.4ns 
534969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535095     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
535095     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
535096     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
535096     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
535633     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
539450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.48s 
539503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
539506     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 
560933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
560934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 410.6ns 
560935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 
564473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
564748     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 268.48ms 
564751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
564751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 325.3ns 
564752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.58s 
568380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
568383     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.2ns 
579542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
579542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.6ns 
579543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.64s 
583225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
584034     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 770.98ms 
584037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
584037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.8ns 
584038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.79s 
587868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
589074     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16s 
589078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
589079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 205ns 
589079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.59s 
592687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
592691     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
592692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
592692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.3ns 
592693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
596110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
596112     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 649.9ns 
596138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
596139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.7ns 
596139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.6s 
599796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
601131     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28s 
601138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
601138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 291.9ns 
601139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.53s 
604684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
604687     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 688.9ns 
604690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
604691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.5ns 
604692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.5s 
608235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
608236     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.5ns 
619450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
619450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.7ns 
619450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 
622982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
624258     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22s