MergeRuleTests

11

tests

0

failures

0

ignored

1m35.29s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 15.522s passed
testDoAutomaticGcdProofWithMergePointStatements() 14.287s passed
testDoManualGcdProof() 29.128s passed
testLoadClosedGcdProofWithMergePointStatements() 4.987s passed
testLoadGcdProof() 4.636s passed
testLoadGcdProofWithPredAbstr() 4.453s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 5.546s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 5.907s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.672s passed
testMergeIndistinguishablePathConditionsWithITE() 3.623s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.527s passed

Standard output

565005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
565005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.1ns 
565005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565165     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
565165     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
565165     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
565165     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
565801     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
569893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.89s 
569940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
569940     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 
594143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
594143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 169.2ns 
594143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.64s 
597846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
600034     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.19s 
600034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
600034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.3ns 
600159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.74s 
603964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
603964     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.1ns 
615571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
615571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.5ns 
615571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
619442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.87s 
619677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
621102     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 856.34ms 
621102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
621102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 410.5ns 
621102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.67s 
624830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
625555     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 694.69ms 
625555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
625555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.9ns 
625571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
629020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
629082     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 524.1ns 
629098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
629098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.3ns 
629098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
632692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.6s 
632723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
632723     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 476ns 
632754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
632754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 409.3ns 
632754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
636428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.66s 
636490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
637663     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03s 
637741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
637741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.1ns 
637741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.6s 
641364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
641364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 225.9ns 
641364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
641364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.1ns 
641364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.66s 
645120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
645120     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.8ns 
655651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
655651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 460.8ns 
655651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
659451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.8s 
659498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
660287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 753.08ms