MergeRuleTests

11

tests

0

failures

0

ignored

1m16.02s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 12.371s passed
testDoAutomaticGcdProofWithMergePointStatements() 11.329s passed
testDoManualGcdProof() 21.472s passed
testLoadClosedGcdProofWithMergePointStatements() 4.639s passed
testLoadGcdProof() 4.302s passed
testLoadGcdProofWithPredAbstr() 4.199s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.480s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.858s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.088s passed
testMergeIndistinguishablePathConditionsWithITE() 3.116s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.168s passed

Standard output

483886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
483886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.2ns 
483886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484059     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
484059     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
484059     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
484059     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
484739     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
488284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.4s 
488322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
488324     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 
505357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
505357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.8ns 
505358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.59s 
508992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
509214     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 217.97ms 
509219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
509220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.2ns 
509220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
512404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
512407     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.1ns 
521590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
521590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 357.5ns 
521591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
524787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
526068     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25s 
526070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
526071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 307ns 
526071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
529316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
530266     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 909.29ms 
530269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
530269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.6ns 
530269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
533428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
533435     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 790.7ns 
533437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
533439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.24ms 
533439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
536501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
536503     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 519.6ns 
536524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
536524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.1ns 
536525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
539967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
541158     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15s 
541164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
541164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.8ns 
541165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
544276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
544279     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 538.7ns 
544280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
544280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
544280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
547504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
547506     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.6ns 
555609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
555609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.5ns 
555610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
558994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
559908     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 878.23ms