MergeRuleTests

11

tests

0

failures

0

ignored

1m26.52s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 14.881s passed
testDoAutomaticGcdProofWithMergePointStatements() 13.986s passed
testDoManualGcdProof() 22.928s passed
testLoadClosedGcdProofWithMergePointStatements() 5.136s passed
testLoadGcdProof() 4.955s passed
testLoadGcdProofWithPredAbstr() 5.134s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.991s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.925s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.475s passed
testMergeIndistinguishablePathConditionsWithITE() 3.645s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.463s passed

Standard output

540345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
540345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.1ns 
540346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540492     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
540493     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
540493     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
540493     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
541085     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
545060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.71s 
545111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
545113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 
563273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
563273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.4ns 
563273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.59s 
566907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
567196     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 285.63ms 
567198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
567199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.5ns 
567199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.63s 
570951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
570954     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.2ns 
582079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
582080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 364.8ns 
582083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.05s 
586182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
587067     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 849.94ms 
587070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
587071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.9ns 
587071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.65s 
590769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
592200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37s 
592204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
592205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.8ns 
592205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
595662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
595665     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
595667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
595667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
595667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 
599112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
599114     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 745.59ns 
599141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
599142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.1ns 
599142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.64s 
602835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
604270     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39s 
604279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
604279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 366ns 
604280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.62s 
607918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
607921     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
607923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
607924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.7ns 
607924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.64s 
611606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
611608     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.6ns 
621911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
621912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 439.79ns 
621912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.65s 
625607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
626860     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21s