MergeRuleTests

11

tests

0

failures

0

ignored

1m47.34s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 16.567s passed
testDoAutomaticGcdProofWithMergePointStatements() 16.388s passed
testDoManualGcdProof() 26.998s passed
testLoadClosedGcdProofWithMergePointStatements() 6.669s passed
testLoadGcdProof() 6.489s passed
testLoadGcdProofWithPredAbstr() 6.585s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 6.274s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 5.886s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 5.173s passed
testMergeIndistinguishablePathConditionsWithITE() 5.099s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 5.209s passed

Standard output

811902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
811902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 510.6ns 
811902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
812113     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
812113     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
812113     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
812113     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
813035     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
818730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.82s 
818777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
818793     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns 
838897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
838897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 180.6ns 
838913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
844402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.49s 
844460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
844783     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 319.78ms 
844783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
844783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.3ns 
844798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
850241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.44s 
850323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
850338     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.5ns 
861350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
861350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.1ns 
861365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
866797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.43s 
866906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
867625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 667.48ms 
867640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
867640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 552.6ns 
867640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
873082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.45s 
873129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
874195     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 972.52ms 
874210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
874210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.5ns 
874210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
879388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.18s 
879419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
879419     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 450.7ns 
879419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
879419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.6ns 
879419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
884545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.11s 
884561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
884561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 378ns 
884592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
884592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 582.9ns 
884592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
889986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.39s 
890033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
891261     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13s 
891261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
891261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.9ns 
891261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
896346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.08s 
896360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
896360     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 353.5ns 
896376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
896376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 499.9ns 
896376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
901709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.33s 
901756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
901756     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.3ns 
912764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
912764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 672.8ns 
912764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
918227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.47s 
918274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
919237     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 874.93ms