MergeRuleTests

11

tests

0

failures

0

ignored

1m31.13s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 14.900s passed
testDoAutomaticGcdProofWithMergePointStatements() 14.556s passed
testDoManualGcdProof() 25.236s passed
testLoadClosedGcdProofWithMergePointStatements() 5.449s passed
testLoadGcdProof() 5.083s passed
testLoadGcdProofWithPredAbstr() 5.598s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.954s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.315s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.611s passed
testMergeIndistinguishablePathConditionsWithITE() 3.659s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.768s passed

Standard output

589313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
589313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 453.6ns 
589313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589469     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
589469     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
589469     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
589469     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
590095     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
594410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.1s 
594472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
594472     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 
614546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
614546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.3ns 
614562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.9s 
618518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
618862     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 327.07ms 
618862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
618862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.8ns 
618862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.84s 
622787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
622787     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.1ns 
633778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
633778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 589.4ns 
633778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.93s 
637765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
638718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 907.43ms 
638718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
638718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 399.3ns 
638718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.99s 
642753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
644316     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5s 
644316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
644316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.5ns 
644332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.72s 
648069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
648084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
648084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
648084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 147.6ns 
648084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
651633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s 
651648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
651664     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 843.3ns 
651695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
651695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 497.1ns 
651695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
655487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.79s 
655643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
657129     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44s 
657144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
657144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 440.8ns 
657144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
660787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.63s 
660803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
660803     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 817.4ns 
660803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
660803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 406.4ns 
660818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
664588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.78s 
664635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
664635     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.2ns 
675359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
675359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 520.4ns 
675374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
679066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.7s 
679113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
680427     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27s