MergeRuleTests

11

tests

0

failures

0

ignored

1m8.53s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 11.569s passed
testDoAutomaticGcdProofWithMergePointStatements() 11.001s passed
testDoManualGcdProof() 19.034s passed
testLoadClosedGcdProofWithMergePointStatements() 3.983s passed
testLoadGcdProof() 3.656s passed
testLoadGcdProofWithPredAbstr() 3.892s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 3.611s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.264s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 2.713s passed
testMergeIndistinguishablePathConditionsWithITE() 2.964s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 2.845s passed

Standard output

451193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
451193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 471.5ns 
451193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451308     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
451308     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
451308     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
451308     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
451897     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
455001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.8s 
455048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
455048     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 
470236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
470236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 506.5ns 
470236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
473213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
473486     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 267.39ms 
473486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
473486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.2ns 
473486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
476378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
476378     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.9ns 
485055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
485055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.3ns 
485055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
488088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
488666     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 544.17ms 
488666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
488666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.2ns 
488666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
491758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
492542     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 757.29ms 
492558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
492558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 446.3ns 
492558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
495395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
495395     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 727.5ns 
495395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
495395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 353.8ns 
495395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
498085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
498101     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 553.7ns 
498116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
498116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 431.7ns 
498116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
501133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
502084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 919.11ms 
502099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
502099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.77ms 
502099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
505054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
505054     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 514.6ns 
505070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
505070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.9ns 
505070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
507830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
507830     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.6ns 
516065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
516065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 598.2ns 
516081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
518900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
519721     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 781.34ms