MergeRuleTests

11

tests

0

failures

0

ignored

1m43.60s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 15.858s passed
testDoAutomaticGcdProofWithMergePointStatements() 15.238s passed
testDoManualGcdProof() 24.640s passed
testLoadClosedGcdProofWithMergePointStatements() 6.713s passed
testLoadGcdProof() 6.558s passed
testLoadGcdProofWithPredAbstr() 6.941s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 6.348s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 5.869s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 5.099s passed
testMergeIndistinguishablePathConditionsWithITE() 5.191s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 5.147s passed

Standard output

803230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
803230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.6ns 
803230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
803418     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
803418     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
803418     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
803418     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
804242     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
809778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.54s 
809825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
809825     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 
827988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
827988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 553.3ns 
827988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
833244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.26s 
833416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
833747     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 337.01ms 
833763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
833763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133ns 
833763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
839090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.34s 
839158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
839161     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.2ns 
849605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
849605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 160.1ns 
849605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
855047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.44s 
855110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
855953     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 780.17ms 
855953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
855953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.9ns 
855969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
861485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.52s 
861532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
862753     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12s 
862894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
862894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.6ns 
862910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
868009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.1s 
868025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
868041     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 883.7ns 
868041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
868041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.9ns 
868041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
873093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.05s 
873109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
873109     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 608ns 
873140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
873140     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 444.6ns 
873140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
878512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.37s 
878560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
879837     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19s 
879853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
879853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.4ns 
879853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
885013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.17s 
885044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
885044     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 605.9ns 
885044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
885044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 432.5ns 
885044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
890169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.11s 
890215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
890215     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.1ns 
900298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
900298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 775.8ns 
900298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
905616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.32s 
905663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
906825     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07s