MergeRuleTests

11

tests

0

failures

0

ignored

57.458s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 9.311s passed
testDoAutomaticGcdProofWithMergePointStatements() 9.372s passed
testDoManualGcdProof() 15.850s passed
testLoadClosedGcdProofWithMergePointStatements() 3.346s passed
testLoadGcdProof() 3.020s passed
testLoadGcdProofWithPredAbstr() 3.194s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 2.938s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 2.875s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 2.514s passed
testMergeIndistinguishablePathConditionsWithITE() 2.538s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 2.500s passed

Standard output

392021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
392021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.2ns 
392022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392114     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
392114     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
392115     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
392115     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
392502     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
395335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
395369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
395371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 
407871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
407872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 385.71ns 
407872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
410498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
410744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 243.47ms 
410746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
410746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 311.3ns 
410747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
413334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
413335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.7ns 
420057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
420057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.8ns 
420058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
422672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
422993     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 297.6ms 
422996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
422996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 350.81ns 
422997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
425749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
426186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 401.3ms 
426189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
426190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.6ns 
426190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
428686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
428688     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 285.5ns 
428689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
428689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.8ns 
428690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
431185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
431187     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 231.5ns 
431203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
431203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95ns 
431204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
433947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
434542     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 562.71ms 
434551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
434551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.3ns 
434551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
437085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
437087     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 233.7ns 
437089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
437089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.4ns 
437089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
439779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
439780     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.4ns 
446461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
446461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.8ns 
446462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
449057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
449477     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 388.7ms