MergeRuleTests

11

tests

0

failures

0

ignored

1m25.96s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 13.232s passed
testDoAutomaticGcdProofWithMergePointStatements() 12.858s passed
testDoManualGcdProof() 21.073s passed
testLoadClosedGcdProofWithMergePointStatements() 5.377s passed
testLoadGcdProof() 5.098s passed
testLoadGcdProofWithPredAbstr() 5.301s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 5.082s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.771s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 4.358s passed
testMergeIndistinguishablePathConditionsWithITE() 4.439s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 4.366s passed

Standard output

672547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
672547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 463ns 
672547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
672703     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
672703     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
672703     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
672703     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
673389     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
678156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.62s 
678202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
678202     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 
693614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
693614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.9ns 
693614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
698069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.45s 
698115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
698384     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 261.82ms 
698386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
698386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.8ns 
698389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
702868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.49s 
702914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
702930     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.9ns 
711617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
711617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 504.1ns 
711633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
716153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.53s 
716200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
716700     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 430.82ms 
716700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
716700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 398.9ns 
716700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
721273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.57s 
721320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
722001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 601.91ms 
722001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
722001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.8ns 
722001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
726351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.35s 
726367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
726367     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 392.9ns 
726367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
726367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.7ns 
726383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
730678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.3s 
730693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
730709     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 259.6ns 
730725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
730725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.4ns 
730725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
735253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.52s 
735300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
736087     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 717.24ms 
736102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
736102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.7ns 
736102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
740525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.42s 
740541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
740541     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 287.7ns 
740541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
740541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 384.4ns 
740556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
744931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.37s 
744962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
744978     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.7ns 
753414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
753414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 630.6ns 
753414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
757848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.44s 
757895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
758497     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 531.7ms