MergeRuleTests

11

tests

0

failures

0

ignored

2m4.72s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 19.863s passed
testDoAutomaticGcdProofWithMergePointStatements() 19.340s passed
testDoManualGcdProof() 33.865s passed
testLoadClosedGcdProofWithMergePointStatements() 7.331s passed
testLoadGcdProof() 6.942s passed
testLoadGcdProofWithPredAbstr() 7.629s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 6.801s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 6.129s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 5.425s passed
testMergeIndistinguishablePathConditionsWithITE() 5.721s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 5.675s passed

Standard output

857875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
857875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 671.5ns 
857875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
858108     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
858108     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
858108     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
858108     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
859109     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
865302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.42s 
865348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
865348     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 
891758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
891758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.9ns 
891758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
897435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.67s 
897497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
897872     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 362.77ms 
897872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
897872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 424.3ns 
897872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
903663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.78s 
903726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
903741     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.3ns 
917735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
917735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.1ns 
917735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
923566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.84s 
923644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
924536     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 832.83ms 
924536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
924536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 383.3ns 
924536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
930588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.04s 
930649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
932165     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42s 
932165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
932165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 583.9ns 
932165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
937809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.63s 
937825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
937840     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.26ms 
937840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
937840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.7ns 
937856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
943203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.36s 
943234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
943234     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 547.6ns 
943265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
943265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.5ns 
943265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
948894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.62s 
948941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
950580     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55s 
950596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
950596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.5ms 
950596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
956270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.66s 
956302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
956317     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 430.7ns 
956333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
956333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 566.6ns 
956333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
962102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.76s 
962149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
962165     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.4ns 
975657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
975657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.3ns 
975657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
981301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.64s 
981364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
982599     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14s