MergeRuleTests

11

tests

0

failures

0

ignored

1m25.05s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 13.220s passed
testDoAutomaticGcdProofWithMergePointStatements() 12.940s passed
testDoManualGcdProof() 20.914s passed
testLoadClosedGcdProofWithMergePointStatements() 5.330s passed
testLoadGcdProof() 5.115s passed
testLoadGcdProofWithPredAbstr() 5.172s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.973s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.725s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 4.181s passed
testMergeIndistinguishablePathConditionsWithITE() 4.158s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 4.324s passed

Standard output

652835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
652835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 223.4ns 
652835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
652997     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
652997     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
652997     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
652997     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
653591     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
658289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.45s 
658320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
658336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.8ns 
673757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
673757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 476.2ns 
673757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
678175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.43s 
678222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
678467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 238.77ms 
678467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
678467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.7ns 
678482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
682875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.4s 
682922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
682922     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.7ns 
691687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
691687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.4ns 
691687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
696108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.42s 
696159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
696660     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 462ms 
696676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
696676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.6ns 
696676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
701121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.45s 
701167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
701833     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 586.99ms 
701833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
701833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 399.6ns 
701833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
706126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.29s 
706141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
706157     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 386.1ns 
706157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
706157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.8ns 
706157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
710291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.14s 
710322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
710322     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 280.3ns 
710338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
710353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 520.1ns 
710353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
714735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.39s 
714782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
715668     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 805.74ms 
715668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
715668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.53ms 
715684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
719811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.13s 
719826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
719826     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 252.1ns 
719826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
719826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.3ns 
719842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
724165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.33s 
724212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
724212     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.9ns 
732766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
732766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.9ns 
732766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
737219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.45s 
737250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
737881     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 547.28ms