MergeRuleTests

11

tests

0

failures

0

ignored

1m38.78s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 15.456s passed
testDoAutomaticGcdProofWithMergePointStatements() 15.257s passed
testDoManualGcdProof() 25.091s passed
testLoadClosedGcdProofWithMergePointStatements() 5.969s passed
testLoadGcdProof() 5.645s passed
testLoadGcdProofWithPredAbstr() 5.947s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 5.651s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 5.320s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 4.764s passed
testMergeIndistinguishablePathConditionsWithITE() 4.885s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 4.790s passed

Standard output

767132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
767132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 553.41ns 
767133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
767358     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
767358     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
767359     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
767359     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
768141     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
773778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.65s 
773831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
773833     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 
792223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
792224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 214.2ns 
792224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
797228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5s 
797280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
797541     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 255.82ms 
797543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
797544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 384.41ns 
797545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
802641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.1s 
802690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
802692     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18ns 
813000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
813000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 433.41ns 
813001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
818020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.02s 
818064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
818647     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 531.33ms 
818650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
818650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
818651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
823713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.06s 
823758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
824594     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 752.98ms 
824597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
824597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
824598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
829362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.76s 
829383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
829385     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 399.41ns 
829387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
829387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.2ns 
829388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
834103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.72s 
834123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
834125     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 360ns 
834151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
834151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.9ns 
834152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
839034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.88s 
839080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
840112     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 950.65ms 
840121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
840121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 320.3ns 
840122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
844981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.86s 
845000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
845003     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 520.81ns 
845004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
845004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
845005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
850055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.05s 
850102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
850104     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.3ns 
860263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
860263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.1ns 
860263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
865045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.78s 
865097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
865903     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 718.82ms