MergeRuleTests

11

tests

0

failures

0

ignored

1m28.80s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 14.292s passed
testDoAutomaticGcdProofWithMergePointStatements() 13.853s passed
testDoManualGcdProof() 23.252s passed
testLoadClosedGcdProofWithMergePointStatements() 5.208s passed
testLoadGcdProof() 4.926s passed
testLoadGcdProofWithPredAbstr() 5.222s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.863s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.657s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 4.113s passed
testMergeIndistinguishablePathConditionsWithITE() 4.206s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 4.205s passed

Standard output

659316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
659316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 490.1ns 
659316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
659472     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
659472     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
659472     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
659472     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
660254     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
664711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.4s 
664758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
664758     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ns 
682565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
682565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 594.7ns 
682580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
686864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.28s 
686911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
687223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 299.85ms 
687223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
687223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.8ns 
687223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
691508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.28s 
691555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
691555     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.9ns 
701515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
701515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.4ns 
701515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
705737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.22s 
705799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
706378     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 524.16ms 
706378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
706378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 522.5ns 
706378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
710803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.42s 
710850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
711600     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 666.76ms 
711600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
711600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 222ns 
711600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
715774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.18s 
715805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
715805     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 870.5ns 
715805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
715805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.2ns 
715821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
719871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.05s 
719886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
719886     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 380.2ns 
719918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
719918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 285.4ns 
719918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
724125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.2s 
724172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
725110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 862.69ms 
725126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
725126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.7ms 
725126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
729316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.18s 
729332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
729332     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 363.5ns 
729332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
729332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 155ns 
729332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
733537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.2s 
733585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
733585     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23ns 
743185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
743185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 630.9ns 
743185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
747375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.18s 
747422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
748111     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 626.5ms