MergeRuleTests

11

tests

0

failures

0

ignored

1m15.77s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 12.715s passed
testDoAutomaticGcdProofWithMergePointStatements() 12.387s passed
testDoManualGcdProof() 21.149s passed
testLoadClosedGcdProofWithMergePointStatements() 4.286s passed
testLoadGcdProof() 3.950s passed
testLoadGcdProofWithPredAbstr() 4.265s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 3.940s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.481s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.096s passed
testMergeIndistinguishablePathConditionsWithITE() 3.311s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.193s passed

Standard output

498279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
498279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.7ns 
498280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498394     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
498394     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
498395     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
498395     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
498916     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
502406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.13s 
502445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
502447     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 
519428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
519428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.7ns 
519429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
522657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
522906     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 246.19ms 
522909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
522909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.1ns 
522910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
526221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
526223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 76.3ns 
535625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
535625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 410.9ns 
535626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
538920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
539562     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 611.2ms 
539565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
539565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 461.3ns 
539566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
542943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
543826     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 843.69ms 
543828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
543828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
543829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
547018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
547021     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 655.6ns 
547022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
547022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
547023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
550094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
550096     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 580ns 
550118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
550118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.8ns 
550119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
553291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
554399     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07s 
554404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
554404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
554405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
557711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
557713     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 841.6ns 
557715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
557715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.5ns 
557717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
560890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
560892     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.1ns 
570102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
570102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.2ns 
570103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
573222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
574050     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 793.22ms