MergeRuleTests

11

tests

0

failures

0

ignored

1m52.79s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 17.472s passed
testDoAutomaticGcdProofWithMergePointStatements() 17.307s passed
testDoManualGcdProof() 27.731s passed
testLoadClosedGcdProofWithMergePointStatements() 7.161s passed
testLoadGcdProof() 6.785s passed
testLoadGcdProofWithPredAbstr() 6.975s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 6.530s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 6.290s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 5.518s passed
testMergeIndistinguishablePathConditionsWithITE() 5.493s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 5.530s passed

Standard output

885544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
885544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 514.1ns 
885544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
885763     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
885763     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
885763     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
885763     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
886730     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
892747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.2s 
892792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
892807     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.4ns 
913271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
913271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.8ns 
913271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
919148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.87s 
919210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
919561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 343.81ms 
919561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
919561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.8ns 
919561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
925237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.67s 
925300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
925300     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.2ns 
937033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
937033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 168.9ns 
937033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
942821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.79s 
942884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
943563     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 627.95ms 
943579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
943579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 518.3ns 
943579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
949499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.93s 
949561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
950538     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 889.86ms 
950538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
950538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 489.1ns 
950538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
956037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.49s 
956053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
956068     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 542.9ns 
956068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
956068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 145ns 
956068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
961540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.46s 
961555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
961555     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 336.1ns 
961586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
961586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.1ns 
961586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
967443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.85s 
967491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
968731     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07s 
968747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
968747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 311.8ns 
968747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
974209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.46s 
974224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
974240     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 349.3ns 
974240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
974240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.36ms 
974240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
979869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.63s 
979916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
979916     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.1ns 
991547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
991547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 229ns 
991547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
997316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.78s 
997373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
998332     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 863.1ms