MergeRuleTests

11

tests

0

failures

0

ignored

1m33.38s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 16.221s passed
testDoAutomaticGcdProofWithMergePointStatements() 14.987s passed
testDoManualGcdProof() 27.933s passed
testLoadClosedGcdProofWithMergePointStatements() 4.865s passed
testLoadGcdProof() 5.093s passed
testLoadGcdProofWithPredAbstr() 5.542s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.318s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.042s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.223s passed
testMergeIndistinguishablePathConditionsWithITE() 3.599s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.555s passed

Standard output

565851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
565851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.6ns 
565851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566009     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
566009     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
566009     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
566009     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
566607     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
570636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.78s 
570683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
570683     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 
593808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
593808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 570.1ns 
593808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.53s 
597383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
597820     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 433.06ms 
597836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
597836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 403.4ns 
597836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.6s 
601597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
601597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.6ns 
614057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
614057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.6ns 
614073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
617562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
618375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 780.51ms 
618375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
618375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 174.6ns 
618375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.83s 
622404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
623917     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22s 
623917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
623917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.1ns 
623917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.53s 
627472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
627472     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 787.1ns 
627472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
627472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 414.7ns 
627472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
630664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
630664     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 520.7ns 
630695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
630695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 462ns 
630695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.56s 
634293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
635560     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21s 
635560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
635560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.51ms 
635575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
639081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.5s 
639097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
639144     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.02ms 
639175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
639175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 510.2ns 
639175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s 
642769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
642769     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.4ns 
654157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
654157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 584.1ns 
654173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
657766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.6s 
657828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
659234     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37s