MergeRuleTests

11

tests

0

failures

0

ignored

1m17.64s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 13.047s passed
testDoAutomaticGcdProofWithMergePointStatements() 12.454s passed
testDoManualGcdProof() 23.180s passed
testLoadClosedGcdProofWithMergePointStatements() 4.058s passed
testLoadGcdProof() 3.906s passed
testLoadGcdProofWithPredAbstr() 3.892s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 3.793s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.472s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.154s passed
testMergeIndistinguishablePathConditionsWithITE() 3.384s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.301s passed

Standard output

487498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
487499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.6ns 
487499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487614     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
487614     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
487614     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
487615     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
488082     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
491537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.04s 
491584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
491586     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 
510679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
510680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 345.61ns 
510680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
513815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
514150     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 330.71ms 
514151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
514151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.3ns 
514156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
517545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
517547     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.5ns 
527198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
527198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
527199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
530344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
530988     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 606.2ms 
530991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
530991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.01ns 
530992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
534217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
534259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
534879     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 564.2ms 
534883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
534884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 333.81ns 
534884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
538180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
538182     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 517.52ns 
538184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
538184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
538184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
541314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
541315     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 262.51ns 
541338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
541338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.9ns 
541339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
544586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
545388     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 745.88ms 
545396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
545397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 336.61ns 
545397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
548775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
548778     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 334.81ns 
548780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
548780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
548780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
551879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
551881     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.8ns 
561234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
561234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
561235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
564530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
565136     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 554.37ms