MergeRuleTests

11

tests

0

failures

0

ignored

1m22.01s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 13.747s passed
testDoAutomaticGcdProofWithMergePointStatements() 14.240s passed
testDoManualGcdProof() 23.069s passed
testLoadClosedGcdProofWithMergePointStatements() 4.463s passed
testLoadGcdProof() 4.566s passed
testLoadGcdProofWithPredAbstr() 4.673s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.139s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.566s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.122s passed
testMergeIndistinguishablePathConditionsWithITE() 3.192s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.237s passed

Standard output

508747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
508747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.5ns 
508748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508889     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
508889     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
508890     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
508890     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
509473     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
512997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.25s 
513049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
513051     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 
531816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
531817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 479.3ns 
531818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
535131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
535379     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 244.28ms 
535382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
535382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 302.4ns 
535383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
538696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
538698     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.6ns 
549135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
549135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 365ns 
549138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
552494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
553271     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 743.17ms 
553274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
553275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 321.4ns 
553275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
556769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
557944     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12s 
557947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
557947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.4ns 
557948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
561173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
561182     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
561184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
561185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 304ns 
561185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
564280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
564282     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 632.9ns 
564306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
564306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.6ns 
564307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
567538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
568761     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17s 
568769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
568770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 293.3ns 
568770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
571956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
571960     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 854.7ns 
571961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
571961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.3ns 
571962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
575279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
575284     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49ns 
586200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
586201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.8ns 
586201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
589663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
590763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05s