MergeRuleTests

11

tests

0

failures

0

ignored

1m32.88s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 15.259s passed
testDoAutomaticGcdProofWithMergePointStatements() 14.839s passed
testDoManualGcdProof() 26.470s passed
testLoadClosedGcdProofWithMergePointStatements() 5.518s passed
testLoadGcdProof() 5.128s passed
testLoadGcdProofWithPredAbstr() 5.409s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 5.065s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.237s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.564s passed
testMergeIndistinguishablePathConditionsWithITE() 3.705s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.690s passed

Standard output

575896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
575896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.7ns 
575911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576161     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
576161     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
576161     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
576161     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
576803     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
581086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.17s 
581164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
581164     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 
602395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
602395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.4ns 
602395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606178     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.79s 
606241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
606616     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 369.11ms 
606616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
606616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 462.4ns 
606631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.79s 
610477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
610477     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18ns 
621875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
621875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.1ns 
621875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.78s 
625721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
626940     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19s 
626956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
626956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 471.5ns 
626956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.8s 
630802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
632335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47s 
632350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
632350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.2ns 
632350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
636008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.65s 
636024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
636040     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
636040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
636040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.3ns 
636040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
639557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 
639573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
639573     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 816ns 
639604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
639604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 153.9ns 
639604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
643309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.7s 
643372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
645107     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69s 
645122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
645122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.3ns 
645122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.67s 
648811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
648811     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 910.4ns 
648827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
648827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.17ms 
648827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
652408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.58s 
652470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
652470     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.4ns 
663666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
663666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228ns 
663666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
667246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.57s 
667293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
668794     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45s