MergeRuleTests

11

tests

0

failures

0

ignored

1m42.60s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 15.797s passed
testDoAutomaticGcdProofWithMergePointStatements() 15.779s passed
testDoManualGcdProof() 25.793s passed
testLoadClosedGcdProofWithMergePointStatements() 6.358s passed
testLoadGcdProof() 6.029s passed
testLoadGcdProofWithPredAbstr() 6.359s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 5.993s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 5.421s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 4.966s passed
testMergeIndistinguishablePathConditionsWithITE() 5.062s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 5.039s passed

Standard output

769046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
769046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.15ms 
769046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
769265     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
769265     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
769265     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
769265     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
770199     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
775589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.55s 
775636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
775651     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 
794839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
794839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 160.1ns 
794839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
799916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.08s 
799963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
800246     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 269.27ms 
800246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
800246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.4ns 
800246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
805257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.01s 
805323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
805324     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.1ns 
816043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
816043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 504.1ns 
816043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
821266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.21s 
821330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
822037     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 641.23ms 
822037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
822037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.1ns 
822037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
827400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.36s 
827447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
828396     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 847.5ms 
828396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
828396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 203.6ns 
828396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
833404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.01s 
833419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
833435     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 398.9ns 
833435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
833435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 407.7ns 
833435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
838353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.91s 
838369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
838369     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 301.6ns 
838401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
838401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 540ns 
838401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
843471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.07s 
843520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
844759     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 995.16ms 
844759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
844759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.4ns 
844759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
849790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.03s 
849821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
849821     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 277.2ns 
849821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
849821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 445.4ns 
849821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
854910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.09s 
854973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
854973     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.1ns 
865600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
865600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 613.9ns 
865600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
870707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.1s 
870754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
871629     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 787.53ms