MergeRuleTests

11

tests

0

failures

0

ignored

1m40.12s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 16.007s passed
testDoAutomaticGcdProofWithMergePointStatements() 15.933s passed
testDoManualGcdProof() 25.516s passed
testLoadClosedGcdProofWithMergePointStatements() 5.723s passed
testLoadGcdProof() 5.816s passed
testLoadGcdProofWithPredAbstr() 5.676s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 6.099s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 5.472s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 4.659s passed
testMergeIndistinguishablePathConditionsWithITE() 4.518s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 4.705s passed

Standard output

655986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
655986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 471.6ns 
656002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
656158     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
656158     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
656158     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
656158     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
656924     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
662006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6s 
662068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
662068     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 
681500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
681500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 169.2ns 
681516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
686065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.55s 
686190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
686972     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 733.76ms 
686972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
686972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 458.6ns 
686988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
691443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.46s 
691521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
691521     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.1ns 
702995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
702995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.2ns 
702995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
707546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.55s 
707593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
709078     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43s 
709078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
709078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 147.1ns 
709078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
713847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.77s 
713909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
714754     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 758.32ms 
714769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
714769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.2ns 
714769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
719443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.67s 
719459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
719459     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 463.5ns 
719459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
719475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 445.3ns 
719475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
724071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.6s 
724087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
724087     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 314.3ns 
724118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
724118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 453.4ns 
724134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
728637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.51s 
728684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
729826     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06s 
729841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
729841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.81ms 
729857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
734328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.48s 
734359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
734359     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 365.1ns 
734359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
734359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.3ns 
734359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
739113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.74s 
739160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
739160     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.9ns 
750292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
750292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.1ns 
750292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
755248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.95s 
755294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
756108     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 728.36ms