MergeRuleTests

11

tests

0

failures

0

ignored

1m10.80s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 11.837s passed
testDoAutomaticGcdProofWithMergePointStatements() 11.607s passed
testDoManualGcdProof() 19.934s passed
testLoadClosedGcdProofWithMergePointStatements() 4.073s passed
testLoadGcdProof() 3.786s passed
testLoadGcdProofWithPredAbstr() 3.972s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 3.621s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.280s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 2.811s passed
testMergeIndistinguishablePathConditionsWithITE() 2.939s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 2.943s passed

Standard output

446659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
446659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 440ns 
446659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446768     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
446768     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
446768     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
446768     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
447280     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
450527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.87s 
450559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
450574     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 
466592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
466592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 455.2ns 
466592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
469557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
469872     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 291.63ms 
469872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
469872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 447.2ns 
469872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
472940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
472940     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.1ns 
481709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
481709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 149ns 
481709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
484744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
485330     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 550.57ms 
485330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
485330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.8ns 
485330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
488481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
489302     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 777.38ms 
489302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
489302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 427.4ns 
489302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
492233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
492248     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 728.4ns 
492248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
492248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 380.7ns 
492248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
495042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
495042     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 554.6ns 
495074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
495074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.3ns 
495076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
498195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
499130     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 903.63ms 
499130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
499145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.73ms 
499145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
502064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
502080     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 581.2ns 
502080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
502080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 399.6ns 
502080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
504984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
505016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
505016     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.7ns 
513677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
513677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 576.3ns 
513677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
516696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
517463     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 730.19ms