MergeRuleTests

11

tests

0

failures

0

ignored

1m28.72s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 14.413s passed
testDoAutomaticGcdProofWithMergePointStatements() 14.103s passed
testDoManualGcdProof() 24.409s passed
testLoadClosedGcdProofWithMergePointStatements() 5.270s passed
testLoadGcdProof() 4.879s passed
testLoadGcdProofWithPredAbstr() 5.284s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 6.130s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.050s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.377s passed
testMergeIndistinguishablePathConditionsWithITE() 3.376s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.424s passed

Standard output

543794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
543794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 496.1ns 
543794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543951     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
543951     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
543951     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
543951     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
544545     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
548455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.66s 
548517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
548517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 
568202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
568202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.29ms 
568217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.64s 
571908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
572252     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 344.55ms 
572252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
572252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.6ns 
572268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.6s 
575910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
575910     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.3ns 
586666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
586666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 147.1ns 
586666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.64s 
590434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
592779     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59s 
592795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
592795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.6ns 
592795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.78s 
596625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
598079     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39s 
598079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
598079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219ns 
598079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
601503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
601503     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
601503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
601503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 400.9ns 
601503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
604849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
604849     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 738ns 
604880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
604880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.5ns 
604880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 
608430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
610150     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66s 
610150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
610150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.4ns 
610165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
613510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
613526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
613526     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 925.9ns 
613526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
613526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 395ns 
613526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.54s 
617122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
617122     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.1ns 
627644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
627644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 728.4ns 
627644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 
631195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
632492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26s