MergeRuleTests

11

tests

0

failures

0

ignored

1m51.19s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 16.773s passed
testDoAutomaticGcdProofWithMergePointStatements() 16.281s passed
testDoManualGcdProof() 27.965s passed
testLoadClosedGcdProofWithMergePointStatements() 7.414s passed
testLoadGcdProof() 6.880s passed
testLoadGcdProofWithPredAbstr() 7.251s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 6.698s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 5.959s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 5.241s passed
testMergeIndistinguishablePathConditionsWithITE() 5.508s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 5.224s passed

Standard output

848599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
848599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.2ns 
848615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
848819     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
848819     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
848819     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
848819     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
849782     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
855530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.92s 
855592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
855592     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 
876574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
876574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 355.7ns 
876574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
882139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.57s 
882202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
882536     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 333.52ms 
882536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
882536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.5ns 
882552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
888036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.49s 
888099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
888099     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16ns 
899312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
899313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 556.4ns 
899316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
904905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.6s 
904967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
905992     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 959.56ms 
906007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
906007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.2ns 
906007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
911662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.66s 
911709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
913258     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44s 
913258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
913258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 394.4ns 
913274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
918436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.17s 
918467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
918467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
918482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
918482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 167.3ns 
918482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
923661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.18s 
923692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
923692     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 652.1ns 
923723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
923723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.7ns 
923723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
929465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.74s 
929512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
931137     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53s 
931137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
931153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 368.6ns 
931153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
936630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.48s 
936645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
936645     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
936661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
936661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 499.6ns 
936661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
941972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.31s 
942018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
942034     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.9ns 
952926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
952942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 5.19ms 
952942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
958333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.39s 
958380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
959808     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35s