MergeRuleTests

11

tests

0

failures

0

ignored

1m26.13s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 13.372s passed
testDoAutomaticGcdProofWithMergePointStatements() 12.968s passed
testDoManualGcdProof() 20.787s passed
testLoadClosedGcdProofWithMergePointStatements() 5.522s passed
testLoadGcdProof() 5.166s passed
testLoadGcdProofWithPredAbstr() 5.254s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 5.150s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.748s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 4.364s passed
testMergeIndistinguishablePathConditionsWithITE() 4.387s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 4.416s passed

Standard output

705753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
705753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 265.6ns 
705753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
705895     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
705895     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
705895     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
705895     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
706497     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
711331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.58s 
711378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
711378     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 
726533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
726533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 215.5ns 
726533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
730999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.47s 
731046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
731281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 229.87ms 
731281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
731281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.4ns 
731296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
735842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.56s 
735889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
735889     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.5ns 
744653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
744653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.2ns 
744669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
749272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.61s 
749319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
749803     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 434.54ms 
749803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
749803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 426.8ns 
749803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
754383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.58s 
754430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
755057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 560.35ms 
755057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
755057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.2ns 
755057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
759457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.39s 
759473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
759473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 361.2ns 
759473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
759488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.6ms 
759488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
763791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.31s 
763822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
763822     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 285.4ns 
763837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
763837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 184.9ns 
763853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
768494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.64s 
768526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
769343     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 741.28ms 
769359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
769359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 190.7ns 
769359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
773730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.38s 
773746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
773746     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 277.3ns 
773762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
773762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 466.8ns 
773762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
778108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.35s 
778140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
778155     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.2ns 
786714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
786714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181ns 
786714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
791159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.45s 
791206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
791864     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 595.77ms