MergeRuleTests

11

tests

0

failures

0

ignored

1m24.38s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 14.574s passed
testDoAutomaticGcdProofWithMergePointStatements() 13.538s passed
testDoManualGcdProof() 24.436s passed
testLoadClosedGcdProofWithMergePointStatements() 4.721s passed
testLoadGcdProof() 4.410s passed
testLoadGcdProofWithPredAbstr() 4.770s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.293s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.711s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.334s passed
testMergeIndistinguishablePathConditionsWithITE() 3.429s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.164s passed

Standard output

510150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
510151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.7ns 
510151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510280     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
510280     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
510281     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
510281     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
510948     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
514775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.62s 
514829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
514832     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 
534587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
534587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.4ns 
534588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
537988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
538296     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 303.44ms 
538300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
538300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.71ns 
538301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s 
541898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
541900     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.3ns 
552872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
552873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 366.71ns 
552875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 
556347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
557161     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 782.06ms 
557165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
557165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 363.71ns 
557166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
560708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
561932     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17s 
561935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
561936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 728.23ns 
561937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
565095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
565098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
565099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
565099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
565100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
568406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
568408     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 666.63ns 
568435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
568436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 438.82ns 
568437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
571882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
573148     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22s 
573155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
573155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.6ns 
573156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
576580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
576583     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 727.23ns 
576584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
576584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
576585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
579859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
579860     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24ns 
590122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
590122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.2ns 
590123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
593494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
594528     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 991.93ms