MergeRuleTests

11

tests

0

failures

0

ignored

1m27.73s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 14.761s passed
testDoAutomaticGcdProofWithMergePointStatements() 14.245s passed
testDoManualGcdProof() 25.175s passed
testLoadClosedGcdProofWithMergePointStatements() 4.987s passed
testLoadGcdProof() 4.768s passed
testLoadGcdProofWithPredAbstr() 4.832s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.455s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.939s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.424s passed
testMergeIndistinguishablePathConditionsWithITE() 3.595s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.549s passed

Standard output

548856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
548856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 455.4ns 
548856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548997     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
548997     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
548997     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
548997     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
549747     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
553718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.86s 
553780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
553780     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 
574025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
574025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 357.4ns 
574025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.57s 
577667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
577964     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 297.43ms 
577964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
577964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 427.7ns 
577964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.66s 
581685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
581686     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.7ns 
592725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
592725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.2ns 
592725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 
596258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
597165     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 707.83ms 
597180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
597180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 438.6ns 
597180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.7s 
600933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
602012     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02s 
602012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
602012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 420.7ns 
602012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s 
605545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
605561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
605561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
605561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 396ns 
605561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
608953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
608953     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 723.2ns 
608985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
608985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.7ns 
608985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 
612565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
613972     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34s 
613972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
613987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.88ms 
613987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.56s 
617567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
617567     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 608.8ns 
617567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
617567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.3ns 
617583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
621023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
621023     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.9ns 
631812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
631812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 597.4ns 
631812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 
635359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
636564     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16s