MergeRuleTests

11

tests

0

failures

0

ignored

1m33.13s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 14.555s passed
testDoAutomaticGcdProofWithMergePointStatements() 13.100s passed
testDoManualGcdProof() 24.910s passed
testLoadClosedGcdProofWithMergePointStatements() 5.908s passed
testLoadGcdProof() 5.221s passed
testLoadGcdProofWithPredAbstr() 5.953s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 6.331s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.658s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 4.191s passed
testMergeIndistinguishablePathConditionsWithITE() 4.286s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 4.018s passed

Standard output

637992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
637992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 408.7ns 
637992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638149     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
638149     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
638149     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
638149     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
638978     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
643948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.96s 
644089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
644089     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.9ns 
662898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
662898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 155.3ns 
662898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
667056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.17s 
667228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
667556     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 284.26ms 
667556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
667556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.1ns 
667556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
671777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.22s 
671918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
671918     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.1ns 
682111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
682111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.2ns 
682111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
686317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.2s 
686364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
688442     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11s 
688458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
688458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 174.3ns 
688458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
692711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.26s 
692758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
694398     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49s 
694398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
694398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.5ns 
694398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
698385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.99s 
698401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
698416     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
698416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
698416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.6ns 
698416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
702560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.15s 
702591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
702591     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 348.9ns 
702607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
702607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 461.2ns 
702622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
707046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.43s 
707093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
708468     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19s 
708515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
708515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.06ms 
708531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
712770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.24s 
712801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
712801     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 342.4ns 
712801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
712801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 405.2ns 
712801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
717053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.24s 
717084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
717100     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.9ns 
725901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
725901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.5ns 
725901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
730200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.29s 
730247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
731107     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 719.76ms