MergeRuleTests

11

tests

0

failures

0

ignored

1m51.98s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 17.645s passed
testDoAutomaticGcdProofWithMergePointStatements() 17.170s passed
testDoManualGcdProof() 28.099s passed
testLoadClosedGcdProofWithMergePointStatements() 7.039s passed
testLoadGcdProof() 6.623s passed
testLoadGcdProofWithPredAbstr() 6.967s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 6.416s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 6.160s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 5.324s passed
testMergeIndistinguishablePathConditionsWithITE() 5.231s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 5.310s passed

Standard output

830092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
830092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.5ns 
830108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
830311     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
830311     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
830311     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
830311     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
831235     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
837206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.1s 
837253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
837253     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 
858204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
858204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233ns 
858204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
863859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.66s 
863922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
864349     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 422.89ms 
864349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
864349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.5ns 
864364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
869920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.56s 
869982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
869998     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.3ns 
881994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
881994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 174.2ns 
881994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
887628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.63s 
887690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
888410     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 651.49ms 
888410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
888410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.7ns 
888410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
894265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.85s 
894312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
895361     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 948.95ms 
895377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
895377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.2ns 
895377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
900672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.29s 
900687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
900687     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 514.1ns 
900703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
900703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.7ns 
900703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
905964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.26s 
905980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
905980     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 317.1ns 
906011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
906011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 651ns 
906011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
911701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.69s 
911748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
913034     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18s 
913050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
913050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.1ns 
913050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
918266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.21s 
918281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
918281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 293.6ns 
918297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
918297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 510.1ns 
918302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
923877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.59s 
923981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
923983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.1ns 
935451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
935451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 679.1ns 
935451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
941076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.61s 
941139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
942074     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 851.39ms