MergeRuleTests

11

tests

0

failures

0

ignored

1m42.56s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 15.945s passed
testDoAutomaticGcdProofWithMergePointStatements() 15.378s passed
testDoManualGcdProof() 24.974s passed
testLoadClosedGcdProofWithMergePointStatements() 6.437s passed
testLoadGcdProof() 6.067s passed
testLoadGcdProofWithPredAbstr() 6.297s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 6.139s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 5.661s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 5.209s passed
testMergeIndistinguishablePathConditionsWithITE() 5.291s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 5.159s passed

Standard output

792254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
792254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 479.7ns 
792254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
792426     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
792426     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
792426     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
792426     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
793142     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
798881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.64s 
798933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
798933     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 
817242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
817242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 501ns 
817242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
822545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.3s 
822591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
822889     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 291.49ms 
822889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
822889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.1ns 
822904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
828178     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.28s 
828225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
828241     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.9ns 
838850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
838850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 507ns 
838850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
844296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.44s 
844348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
844974     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 568.28ms 
844989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
844989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.8ns 
844989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
850442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.46s 
850504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
851271     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 679.54ms 
851287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
851287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 445.1ns 
851287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
856399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.11s 
856415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
856415     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 395.4ns 
856430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
856430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187ns 
856430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
861577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.16s 
861608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
861608     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 294.8ns 
861639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
861639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 510.8ns 
861639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
867061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.43s 
867124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
868076     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 862.74ms 
868076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
868092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.6ns 
868092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
873335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.25s 
873367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
873367     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 285.3ns 
873367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
873367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 423.7ns 
873367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
878545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.18s 
878592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
878608     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.2ns 
888761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
888761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 842.9ns 
888761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
894043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.28s 
894089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
894812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 633.78ms