MergeRuleTests

11

tests

0

failures

0

ignored

1m28.23s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 13.652s passed
testDoAutomaticGcdProofWithMergePointStatements() 13.183s passed
testDoManualGcdProof() 21.700s passed
testLoadClosedGcdProofWithMergePointStatements() 5.670s passed
testLoadGcdProof() 5.302s passed
testLoadGcdProofWithPredAbstr() 5.456s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 5.138s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.734s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 4.381s passed
testMergeIndistinguishablePathConditionsWithITE() 4.579s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 4.433s passed

Standard output

677977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
677977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 168.2ns 
677977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
678134     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
678134     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
678134     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
678134     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
678769     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
683619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.65s 
683666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
683666     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns 
699670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
699670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.9ns 
699685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
704074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.4s 
704121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
704404     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 269.6ms 
704420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
704420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 674ns 
704436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
708907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.48s 
709039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
709042     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.4ns 
718056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
718056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 168ns 
718056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
722615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.56s 
722677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
723194     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 473.62ms 
723209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
723209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 395.6ns 
723209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
727911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.71s 
727958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
728650     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 605.33ms 
728666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
728666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 457.3ns 
728666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
733068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.4s 
733083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
733083     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 395.4ns 
733083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
733083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131ns 
733099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
737418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.33s 
737449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
737449     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 299.3ns 
737464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
737464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.8ns 
737464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
742149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.68s 
742196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
743119     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 844.46ms 
743134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
743134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.7ns 
743134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
747682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.55s 
747697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
747697     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 254.9ns 
747713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
747713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 378.1ns 
747713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
752187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.47s 
752234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
752234     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19ns 
760896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
760896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 490.1ns 
760896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
765526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.63s 
765573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
766198     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 556.66ms