MergeRuleTests

11

tests

0

failures

0

ignored

1m10.52s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 12.162s passed
testDoAutomaticGcdProofWithMergePointStatements() 11.607s passed
testDoManualGcdProof() 20.004s passed
testLoadClosedGcdProofWithMergePointStatements() 3.908s passed
testLoadGcdProof() 3.768s passed
testLoadGcdProofWithPredAbstr() 4.002s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 3.534s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.049s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 2.823s passed
testMergeIndistinguishablePathConditionsWithITE() 2.932s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 2.727s passed

Standard output

431928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
431928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 404.1ns 
431944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432131     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
432131     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
432131     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
432131     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
432574     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
435681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.74s 
435713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
435728     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 
451940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
451940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 160.3ns 
451940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
454724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
454989     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 256.58ms 
455005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
455005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 423.3ns 
455005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
457896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
457912     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18ns 
467152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
467152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143ns 
467152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
470030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
470686     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 632.55ms 
470702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
470702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.4ns 
470702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
473797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
474688     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 834.61ms 
474688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
474688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.6ns 
474688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
477408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
477408     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
477423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
477423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.5ns 
477423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
480222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
480222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 721.5ns 
480238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
480253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 432ns 
480253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
483146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
484131     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 948.31ms 
484146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
484146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.2ns 
484146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
487069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
487069     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 599.8ns 
487069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
487069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.6ns 
487085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
489837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
489837     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.1ns 
498685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
498685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 184.6ns 
498701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
501625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
502453     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 786.16ms