MergeRuleTests

11

tests

0

failures

0

ignored

1m25.44s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 13.750s passed
testDoAutomaticGcdProofWithMergePointStatements() 14.069s passed
testDoManualGcdProof() 24.783s passed
testLoadClosedGcdProofWithMergePointStatements() 4.991s passed
testLoadGcdProof() 4.629s passed
testLoadGcdProofWithPredAbstr() 4.515s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.534s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.492s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.324s passed
testMergeIndistinguishablePathConditionsWithITE() 3.237s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.113s passed

Standard output

526103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
526103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 445.8ns 
526103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526235     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
526235     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
526235     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
526235     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
526704     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
530465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.36s 
530512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
530512     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 
550881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
550881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 450.1ns 
550881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
554387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
555373     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 898.33ms 
555373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
555373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 402.2ns 
555373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.58s 
558999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
558999     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.8ns 
569123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
569123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.24ms 
569123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.69s 
572862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
573657     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 752.51ms 
573657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
573657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.6ns 
573657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.54s 
577249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
578156     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 860.79ms 
578172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
578172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.8ns 
578172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
581285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
581285     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 814.2ns 
581285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
581285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 408.1ns 
581301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
584436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
584577     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 89.55ms 
584609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
584609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.8ns 
584609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.79s 
588441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
589585     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09s 
589600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
589600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.4ns 
589600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
592837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
592837     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 492.1ns 
592837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
592837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 366.1ns 
592837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
596252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
596253     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.4ns 
606906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
606906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 418ns 
606906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.64s 
610590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
611535     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 863.48ms