MergeRuleTests

11

tests

0

failures

0

ignored

1m54.38s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 17.908s passed
testDoAutomaticGcdProofWithMergePointStatements() 17.317s passed
testDoManualGcdProof() 28.925s passed
testLoadClosedGcdProofWithMergePointStatements() 7.082s passed
testLoadGcdProof() 6.666s passed
testLoadGcdProofWithPredAbstr() 6.906s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 6.682s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 6.068s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 5.707s passed
testMergeIndistinguishablePathConditionsWithITE() 5.548s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 5.569s passed

Standard output

854540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
854540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 577ns 
854540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
854746     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
854746     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
854746     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
854746     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
855584     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
861758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.21s 
861805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
861821     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.3ns 
883463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
883463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.2ns 
883463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
889124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.66s 
889187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
889531     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 334.78ms 
889531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
889531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.4ns 
889531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
895263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.72s 
895326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
895326     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.1ns 
907439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
907439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 169.6ns 
907455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
913162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.72s 
913225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
914121     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 823.7ms 
914121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
914121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 591.6ns 
914121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
919944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.82s 
920006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
921027     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 926.44ms 
921027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
921027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 502.1ns 
921027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
926565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.54s 
926596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
926596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 465.1ns 
926596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
926611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.45ms 
926611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
932242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.64s 
932272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
932272     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 405.4ns 
932319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
932319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 538.4ns 
932319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
938085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.77s 
938148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
939370     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13s 
939385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
939385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 693.8ns 
939385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
944902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.52s 
944933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
944933     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 346.5ns 
944933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
944933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.8ns 
944933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
950467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.53s 
950528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
950528     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24ns 
962250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
962250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 517.8ns 
962250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
967837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.58s 
967884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
968916     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 952.55ms