MergeRuleTests

11

tests

0

failures

0

ignored

1m6.75s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 11.098s passed
testDoAutomaticGcdProofWithMergePointStatements() 10.857s passed
testDoManualGcdProof() 18.988s passed
testLoadClosedGcdProofWithMergePointStatements() 3.752s passed
testLoadGcdProof() 3.549s passed
testLoadGcdProofWithPredAbstr() 3.768s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 3.455s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.096s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 2.551s passed
testMergeIndistinguishablePathConditionsWithITE() 2.713s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 2.921s passed

Standard output

441300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
441300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.1ns 
441300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441410     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
441410     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
441410     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
441410     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
441925     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
444943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.65s 
444989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
444989     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 
460278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
460278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.2ns 
460278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
463109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
463374     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 254.74ms 
463374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
463374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.7ns 
463374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
466156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
466156     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.5ns 
474472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
474488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 200.2ns 
474488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
477302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
477927     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 587.59ms 
477927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
477927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.6ns 
477943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
480789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
481695     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 853.21ms 
481695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
481695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.3ns 
481695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
484603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
484618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
484618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
484618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.1ns 
484618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
487151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
487151     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 593.7ns 
487167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
487182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 394ns 
487182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
489919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
490919     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 948.55ms 
490919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
490919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.9ns 
490935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
493640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
493640     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 512.6ns 
493640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
493640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86ns 
493640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
496329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
496329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.4ns 
504490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
504490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.3ns 
504490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
507226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
508039     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 764.54ms