MergeRuleTests

11

tests

0

failures

0

ignored

1m34.58s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 15.212s passed
testDoAutomaticGcdProofWithMergePointStatements() 14.698s passed
testDoManualGcdProof() 24.597s passed
testLoadClosedGcdProofWithMergePointStatements() 5.581s passed
testLoadGcdProof() 5.318s passed
testLoadGcdProofWithPredAbstr() 5.659s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 5.472s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.831s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 4.333s passed
testMergeIndistinguishablePathConditionsWithITE() 4.378s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 4.503s passed

Standard output

686423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
686423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.2ns 
686423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
686688     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
686688     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
686688     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
686688     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
687329     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
692099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.68s 
692146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
692161     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 
711016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
711016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.5ns 
711016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
715503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.49s 
715565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
715847     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 275.76ms 
715847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
715847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 147ns 
715863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
720413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.55s 
720460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
720460     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.5ns 
731059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
731059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.2ns 
731059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
735734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.68s 
735937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
736531     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 532.11ms 
736531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
736531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.7ns 
736531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
741174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.64s 
741237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
742175     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 841.04ms 
742190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
742190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.7ns 
742190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
746677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.48s 
746693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
746693     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 589.6ns 
746693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
746693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.6ns 
746708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
750979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.27s 
750994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
750994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 329.8ns 
751026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
751026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 487ns 
751026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
755606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.57s 
755637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
756591     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 868.83ms 
756607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
756607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.4ns 
756607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
760954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.34s 
760969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
760985     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 317.5ns 
760985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
760985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.7ns 
760985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
765347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.36s 
765394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
765394     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.8ns 
775683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
775683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.8ns 
775683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
780219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.53s 
780266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
781001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 647.27ms