MergeRuleTests

11

tests

0

failures

0

ignored

1m54.86s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 19.071s passed
testDoAutomaticGcdProofWithMergePointStatements() 18.056s passed
testDoManualGcdProof() 30.376s passed
testLoadClosedGcdProofWithMergePointStatements() 6.770s passed
testLoadGcdProof() 6.099s passed
testLoadGcdProofWithPredAbstr() 6.801s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 6.361s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 5.893s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 5.019s passed
testMergeIndistinguishablePathConditionsWithITE() 5.238s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 5.176s passed

Standard output

810166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
810166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.2ms 
810166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
810400     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
810400     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
810400     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
810400     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
811447     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
817064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.9s 
817127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
817127     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 
840560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
840560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 451.2ns 
840560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
846016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.45s 
846063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
846438     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 355.28ms 
846438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
846438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 145ns 
846438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
851752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.31s 
851893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
851893     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.3ns 
865509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
865509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.2ns 
865509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
870948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.43s 
871027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
871870     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 770.47ms 
871870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
871870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 440.8ns 
871870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
877358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.48s 
877405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
878671     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14s 
878671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
878671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 511.8ns 
878671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
883816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.14s 
883832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
883847     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
883847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
883847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.8ns 
883863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
888804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.95s 
888835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
888835     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 554ns 
888866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
888866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 631.1ns 
888882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
894197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.33s 
894260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
895621     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27s 
895636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
895636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 444.5ns 
895636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
900843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.21s 
900874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
900874     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 564ns 
900874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
900874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 526.4ns 
900890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
905894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.01s 
905956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
905956     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.2ns 
918932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
918932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.5ns 
918932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
923906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.98s 
923953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
925031     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 976.84ms