MergeRuleTests

11

tests

0

failures

0

ignored

1m32.89s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 15.246s passed
testDoAutomaticGcdProofWithMergePointStatements() 14.353s passed
testDoManualGcdProof() 23.000s passed
testLoadClosedGcdProofWithMergePointStatements() 5.758s passed
testLoadGcdProof() 5.512s passed
testLoadGcdProofWithPredAbstr() 6.016s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 5.201s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.824s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 4.180s passed
testMergeIndistinguishablePathConditionsWithITE() 4.292s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 4.510s passed

Standard output

663956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
663956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.61ns 
663956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
664111     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
664111     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
664112     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
664112     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
664697     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
669438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.48s 
669484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
669486     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 
686956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
686956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.61ns 
686957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
691396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.44s 
691458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
691778     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 310.82ms 
691781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
691781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.92ns 
691786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
696458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.67s 
696537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
696539     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.1ns 
707026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
707026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 454.43ns 
707027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
711620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.59s 
711666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
712223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 495.76ms 
712228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
712228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 381.52ns 
712229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
716573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.34s 
716619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
718238     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41s 
718243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
718243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 378.52ns 
718244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
722727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.48s 
722748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
722751     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 597.63ns 
722753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
722753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.91ns 
722753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
726886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.13s 
726906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
726908     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 302.62ns 
726933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
726933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.31ns 
726933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
731545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.61s 
731595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
732679     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 981.07ms 
732691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
732691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.11ns 
732692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
736960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.27s 
736979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
736981     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 288.32ns 
736982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
736982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88ns 
736983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
741579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.6s 
741624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
741626     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16ns 
751336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
751336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.51ns 
751336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
755740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.4s 
755785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
756843     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 892.19ms