MergeRuleTests

11

tests

0

failures

0

ignored

1m26.81s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 14.096s passed
testDoAutomaticGcdProofWithMergePointStatements() 14.363s passed
testDoManualGcdProof() 25.604s passed
testLoadClosedGcdProofWithMergePointStatements() 4.804s passed
testLoadGcdProof() 4.595s passed
testLoadGcdProofWithPredAbstr() 4.857s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.448s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.716s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.294s passed
testMergeIndistinguishablePathConditionsWithITE() 3.442s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.587s passed

Standard output

521663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
521663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.3ns 
521664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521800     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
521801     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
521802     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
521802     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
522358     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
526203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.54s 
526271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
526273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 
547267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
547267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.1ns 
547268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
550722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
550981     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 255.35ms 
550984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
550985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 380.5ns 
550986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 
554495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
554498     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.1ns 
565080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
565081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 407.2ns 
565081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.59s 
568721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
569525     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 770.63ms 
569529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
569529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 296.5ns 
569530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 
573096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
574382     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22s 
574386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
574386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.9ns 
574386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.47s 
577967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
577970     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
577972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
577972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.9ns 
577973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
581238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
581241     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 771.4ns 
581266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
581267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 445.8ns 
581268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 
584762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
586062     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25s 
586070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
586070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 326.9ns 
586071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
589506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
589510     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
589512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
589512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
589512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.73s 
593304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
593307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.2ns 
603876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
603876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 389.8ns 
603877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
607212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
608466     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21s