MergeRuleTests

11

tests

0

failures

0

ignored

1m18.58s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 13.618s passed
testDoAutomaticGcdProofWithMergePointStatements() 12.678s passed
testDoManualGcdProof() 22.301s passed
testLoadClosedGcdProofWithMergePointStatements() 4.603s passed
testLoadGcdProof() 4.422s passed
testLoadGcdProofWithPredAbstr() 4.195s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.036s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.555s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.148s passed
testMergeIndistinguishablePathConditionsWithITE() 3.032s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 2.995s passed

Standard output

493551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
493551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.5ns 
493551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493692     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
493692     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
493692     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
493692     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
494208     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
497901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.35s 
498214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
498230     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 
515846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
515846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 164ns 
515861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
519104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
519401     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 291.71ms 
519401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
519401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.4ns 
519401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
522765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
522766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.7ns 
533019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
533019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.4ns 
533035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
536399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
537055     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 628.31ms 
537055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
537055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 427.1ns 
537071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
540331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
541250     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 882.81ms 
541250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
541250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.3ns 
541265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
544244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
544244     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 804.7ns 
544260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
544260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 392.1ns 
544260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
547339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
547355     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 695.5ns 
547395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
547396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 458.3ns 
547398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.5s 
550934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
551981     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01s 
551997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
551997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 629.5ns 
551997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
555013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
555029     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 583.7ns 
555029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
555029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 534.8ns 
555029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
558156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
558156     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.7ns 
567707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
567707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 448.4ns 
567707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
571138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
572129     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 890.3ms