MergeRuleTests

11

tests

0

failures

0

ignored

1m19.85s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 13.754s passed
testDoAutomaticGcdProofWithMergePointStatements() 13.505s passed
testDoManualGcdProof() 22.872s passed
testLoadClosedGcdProofWithMergePointStatements() 4.403s passed
testLoadGcdProof() 4.166s passed
testLoadGcdProofWithPredAbstr() 4.405s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 3.992s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.460s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 2.974s passed
testMergeIndistinguishablePathConditionsWithITE() 3.082s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.232s passed

Standard output

528386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
528386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 442.5ns 
528402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528519     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
528519     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
528519     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
528519     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
529035     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
532577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.18s 
532623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
532623     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 
551299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
551299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.9ns 
551299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
554446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
554728     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 267.63ms 
554728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
554728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 346.5ns 
554728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
557916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
557916     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.1ns 
568482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
568482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.7ns 
568482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
571708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
572474     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 738.44ms 
572474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
572474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 365.7ns 
572474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
575835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
576879     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 997.42ms 
576879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
576894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 7.33ms 
576894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
580111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
580111     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 686.9ns 
580111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
580111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.6ns 
580111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
583056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
583072     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 511.1ns 
583088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
583088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 375.6ns 
583088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
586381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
587488     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07s 
587488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
587488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.6ns 
587488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
590570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
590570     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 473.7ns 
590570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
590570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 351.7ns 
590570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
593854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
593854     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.1ns 
604075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
604075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 539.8ns 
604075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
607311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
608225     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 886.55ms