MergeRuleTests

11

tests

0

failures

0

ignored

1m11.64s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 12.163s passed
testDoAutomaticGcdProofWithMergePointStatements() 11.777s passed
testDoManualGcdProof() 20.909s passed
testLoadClosedGcdProofWithMergePointStatements() 3.893s passed
testLoadGcdProof() 3.737s passed
testLoadGcdProofWithPredAbstr() 4.034s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 3.549s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.079s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 2.820s passed
testMergeIndistinguishablePathConditionsWithITE() 2.949s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 2.731s passed

Standard output

451916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
451916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 419.7ns 
451916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452025     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
452025     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
452025     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
452025     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
452463     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
455700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.78s 
455746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
455746     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 
472820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
472820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.3ns 
472820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
475649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
475899     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 248.83ms 
475899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
475899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 385.8ns 
475915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
478823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
478839     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.5ns 
488062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
488062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.4ns 
488062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
490970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
491611     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 601.96ms 
491611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
491611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.8ns 
491611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
494754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
495645     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 843.34ms 
495645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
495645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 404.4ns 
495645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
498367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
498367     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
498383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
498383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.9ns 
498383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
501181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
501181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 684.1ns 
501212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
501212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.9ns 
501212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
504057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
504104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
505073     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 931.42ms 
505089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
505089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 590.7ns 
505089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
508028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
508044     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 802.4ns 
508044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
508044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 398.2ns 
508044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
510780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
510780     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16ns 
519816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
519816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.2ns 
519816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
522678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
523553     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 829.18ms