MergeRuleTests

11

tests

0

failures

0

ignored

1m38.58s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 16.653s passed
testDoAutomaticGcdProofWithMergePointStatements() 16.182s passed
testDoManualGcdProof() 28.179s passed
testLoadClosedGcdProofWithMergePointStatements() 5.506s passed
testLoadGcdProof() 5.286s passed
testLoadGcdProofWithPredAbstr() 5.862s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 5.048s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.420s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.675s passed
testMergeIndistinguishablePathConditionsWithITE() 3.940s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.830s passed

Standard output

587807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
587807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 490.5ns 
587822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587979     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
587979     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
587979     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
587979     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
588667     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
592920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.11s 
593014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
593014     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 
615982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
615982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 487.4ns 
615982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
619953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.96s 
620046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
620406     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 350.4ms 
620406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
620406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 420.5ns 
620406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.86s 
624331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
624331     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.8ns 
637059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
637076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 543.5ns 
637076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.97s 
641107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
642108     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 957.72ms 
642108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
642108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 503.9ns 
642123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
646313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.2s 
646376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
647970     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53s 
647970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
647970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.2ns 
647985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
651769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.79s 
651800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
651800     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
651800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
651800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 426.3ns 
651800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
655412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.61s 
655443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
655459     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
655475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
655475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.4ns 
655490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
659402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.92s 
659464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
660965     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45s 
660981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
660981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.7ns 
660981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
664890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.9s 
664905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
664921     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 810.9ns 
664921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
664921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 402ns 
664921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
668658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.74s 
668720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
668720     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.4ns 
681103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
681103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 586.8ns 
681103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
684997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.89s 
685044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
686389     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29s