MergeRuleTests

11

tests

0

failures

0

ignored

1m26.69s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 13.477s passed
testDoAutomaticGcdProofWithMergePointStatements() 13.102s passed
testDoManualGcdProof() 21.500s passed
testLoadClosedGcdProofWithMergePointStatements() 5.430s passed
testLoadGcdProof() 5.095s passed
testLoadGcdProofWithPredAbstr() 5.148s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 5.094s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.676s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 4.273s passed
testMergeIndistinguishablePathConditionsWithITE() 4.459s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 4.436s passed

Standard output

670599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
670599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.61ns 
670600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
670761     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
670761     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
670762     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
670762     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
671373     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
676188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.59s 
676231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
676233     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 
692099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
692100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 374.52ns 
692101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
696508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.41s 
696551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
696773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 217.6ms 
696775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
696775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 413.52ns 
696779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
701297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.52s 
701341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
701343     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20ns 
710251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
710252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.91ns 
710252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
714699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.45s 
714741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
715343     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 548.26ms 
715346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
715346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.71ns 
715347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
719794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.45s 
719835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
720491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 570.39ms 
720494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
720494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.51ns 
720494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
724907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.41s 
724926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
724928     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 366.62ns 
724930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
724930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
724931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
729159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.23s 
729177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
729179     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 298.62ns 
729203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
729203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.01ns 
729204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
733741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.54s 
733782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
734625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 761.82ms 
734632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
734633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.71ns 
734633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
739071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.44s 
739088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
739090     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 254.22ns 
739092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
739092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
739093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
743460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.37s 
743500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
743502     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.8ns 
752194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
752194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.91ns 
752195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
756617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.42s 
756657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
757285     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 549.18ms