MergeRuleTests

11

tests

0

failures

0

ignored

1m26.86s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 15.171s passed
testDoAutomaticGcdProofWithMergePointStatements() 13.920s passed
testDoManualGcdProof() 25.349s passed
testLoadClosedGcdProofWithMergePointStatements() 4.662s passed
testLoadGcdProof() 4.689s passed
testLoadGcdProofWithPredAbstr() 5.085s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.119s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.728s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.142s passed
testMergeIndistinguishablePathConditionsWithITE() 3.552s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.447s passed

Standard output

523430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
523430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 752.5ns 
523430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523546     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
523562     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
523562     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
523562     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
524074     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
527860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.44s 
527907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
527907     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 
548775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
548775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 485.2ns 
548775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
552206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
552503     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 293.4ms 
552503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
552503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.5ns 
552503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s 
556124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
556311     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.1ns 
567674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
567674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.5ns 
567674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
571105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
571793     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 654.1ms 
571793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
571793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 150ns 
571793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.03s 
575875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
576878     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 954.22ms 
576878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
576878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 374.2ns 
576878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
580325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
580325     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 778.3ns 
580325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
580325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 327.1ns 
580325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
583451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
583451     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 642.1ns 
583467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
583467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 242ns 
583484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 
586966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
588129     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11s 
588144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
588144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 442.8ns 
588144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 
591681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
591681     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 549.6ns 
591681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
591681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 390.5ns 
591681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
595057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
595073     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.1ns 
605601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
605601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 486.1ns 
605601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.57s 
609268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
610290     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 974.84ms