MergeRuleTests

11

tests

0

failures

0

ignored

1m11.07s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 12.148s passed
testDoAutomaticGcdProofWithMergePointStatements() 11.866s passed
testDoManualGcdProof() 20.266s passed
testLoadClosedGcdProofWithMergePointStatements() 4.001s passed
testLoadGcdProof() 3.736s passed
testLoadGcdProofWithPredAbstr() 4.003s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 3.453s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.142s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 2.677s passed
testMergeIndistinguishablePathConditionsWithITE() 2.892s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 2.888s passed

Standard output

428825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
428825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 383.9ns 
428825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428934     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
428934     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
428934     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
428934     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
429356     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
432561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.73s 
432608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
432608     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 
449085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
449085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.9ns 
449085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
451961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
452227     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 261.85ms 
452227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
452227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.1ns 
452227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
455136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
455136     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.2ns 
464375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
464375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 445.1ns 
464375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
467235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
467829     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 569.41ms 
467829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
467829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 409.2ns 
467845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
470752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
471832     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04s 
471847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
471847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 428.1ns 
471847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
474724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
474724     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
474724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
474724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.5ns 
474724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
477381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
477381     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 563.6ns 
477397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
477397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.4ns 
477413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
480398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
481382     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 945.9ms 
481398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
481398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.31ms 
481398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
484291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
484291     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 599.9ns 
484291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
484291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.7ns 
484291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
487151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
487151     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.2ns 
496157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
496157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 610.5ns 
496157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
499080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
499893     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 775.37ms