MergeRuleTests

11

tests

0

failures

0

ignored

1m23.69s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 13.762s passed
testDoAutomaticGcdProofWithMergePointStatements() 13.643s passed
testDoManualGcdProof() 23.021s passed
testLoadClosedGcdProofWithMergePointStatements() 5.111s passed
testLoadGcdProof() 4.835s passed
testLoadGcdProofWithPredAbstr() 4.740s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.432s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.789s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.527s passed
testMergeIndistinguishablePathConditionsWithITE() 3.382s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.448s passed

Standard output

519867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
519867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 367.7ns 
519868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520011     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
520012     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
520013     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
520013     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
520593     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
524403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.54s 
524456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
524458     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 
542889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
542889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 433.3ns 
542890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 
546419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
546675     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 252.1ms 
546677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
546677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 365.4ns 
546678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 
550240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
550242     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.2ns 
560439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
560439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 422.8ns 
560440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 
563948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
564868     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 879.46ms 
564871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
564872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 391.5ns 
564872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 
568372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
569607     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17s 
569611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
569611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.8ns 
569612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 
573054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
573057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
573059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
573059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.6ns 
573059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 
576558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
576562     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 758.3ns 
576586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
576586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.9ns 
576586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.56s 
580194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
581678     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42s 
581704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
581704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 380.3ns 
581705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
585080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
585084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 921.91ns 
585086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
585086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 420.3ns 
585087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
588571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
588572     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15ns 
598730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
598730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 366.2ns 
598731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.5s 
602281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
603556     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22s