MergeRuleTests

11

tests

0

failures

0

ignored

1m25.70s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 13.170s passed
testDoAutomaticGcdProofWithMergePointStatements() 12.981s passed
testDoManualGcdProof() 20.992s passed
testLoadClosedGcdProofWithMergePointStatements() 5.358s passed
testLoadGcdProof() 5.160s passed
testLoadGcdProofWithPredAbstr() 5.253s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.976s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.834s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 4.238s passed
testMergeIndistinguishablePathConditionsWithITE() 4.348s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 4.389s passed

Standard output

656212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
656212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.3ns 
656212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
656363     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
656363     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
656363     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
656363     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
656941     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
661609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.4s 
661640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
661640     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 
677196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
677196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.4ns 
677196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
681696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.5s 
681727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
682029     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 280.63ms 
682031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
682031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.8ns 
682033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
686491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.47s 
686538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
686553     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.5ns 
695200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
695200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 487ns 
695200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
699630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.42s 
699677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
700177     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 444.85ms 
700177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
700177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 488.8ns 
700177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
704695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.52s 
704742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
705430     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 609ms 
705430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
705430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.6ns 
705446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
709788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.35s 
709804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
709804     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 329.5ns 
709819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
709819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129ns 
709819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
714010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.2s 
714026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
714026     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 264.4ns 
714057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
714057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 485.2ns 
714057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
718520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.47s 
718567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
719399     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 762.28ms 
719415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
719415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.65ms 
719415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
723748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.32s 
723764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
723764     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 235.5ns 
723764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
723764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 407.4ns 
723764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
728131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.36s 
728177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
728177     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.8ns 
736745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
736745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 670.5ns 
736745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
741204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.45s 
741235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
741905     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 585.36ms