MergeRuleTests

11

tests

0

failures

0

ignored

1m3.76s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 10.286s passed
testDoAutomaticGcdProofWithMergePointStatements() 10.147s passed
testDoManualGcdProof() 18.667s passed
testLoadClosedGcdProofWithMergePointStatements() 3.370s passed
testLoadGcdProof() 3.113s passed
testLoadGcdProofWithPredAbstr() 3.541s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 3.442s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 2.939s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 2.771s passed
testMergeIndistinguishablePathConditionsWithITE() 2.899s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 2.580s passed

Standard output

418753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
418753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.6ns 
418753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418856     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
418856     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
418856     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
418856     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
419314     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
422350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.6s 
422385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
422387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ns 
437420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
437420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 333.2ns 
437421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
440160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
440357     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 194.4ms 
440359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
440359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.9ns 
440360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
443017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
443019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.9ns 
450645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
450645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
450647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
453653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
454084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 401.63ms 
454087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
454087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.9ns 
454088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
456949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
457625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 527.93ms 
457628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
457628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 275.3ns 
457629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
460205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
460207     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 293.4ns 
460208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
460208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48ns 
460208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
462951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
462956     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 229.1ns 
462979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
462979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
462979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
465697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
466343     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 607.39ms 
466349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
466349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.7ns 
466350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
469244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
469246     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 218.6ns 
469248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
469248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.8ns 
469249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
471970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
471971     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.2ns 
479394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
479394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.8ns 
479395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
481989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
482506     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 485.63ms