MergeRuleTests

11

tests

0

failures

0

ignored

1m23.72s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 14.095s passed
testDoAutomaticGcdProofWithMergePointStatements() 13.634s passed
testDoManualGcdProof() 23.290s passed
testLoadClosedGcdProofWithMergePointStatements() 4.866s passed
testLoadGcdProof() 4.800s passed
testLoadGcdProofWithPredAbstr() 5.476s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.677s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.538s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.005s passed
testMergeIndistinguishablePathConditionsWithITE() 3.105s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.230s passed

Standard output

493437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
493437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.1ns 
493438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493582     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
493582     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
493583     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
493583     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
494196     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
498027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.59s 
498110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
498112     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 
516728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
516728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.3ns 
516729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
519989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
520264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 271.73ms 
520266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
520266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
520271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
523730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
523756     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15ns 
534362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
534363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 387.21ns 
534363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s 
537961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
539035     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04s 
539039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
539039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 315.31ns 
539040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
542233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
544511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.19s 
544515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
544516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 347.01ns 
544516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
547741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
547744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
547745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
547745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
547746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
550725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
550727     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 714.72ns 
550751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
550751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 378.11ns 
550752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
554154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
555609     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41s 
555616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
555617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 463.31ns 
555618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
558717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
558719     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 653.36ns 
558720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
558720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.91ns 
558721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
562158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
562160     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.5ns 
572355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
572355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.2ns 
572356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.67s 
576072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
577151     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03s