MergeRuleTests

11

tests

0

failures

0

ignored

1m50.73s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 16.963s passed
testDoAutomaticGcdProofWithMergePointStatements() 17.113s passed
testDoManualGcdProof() 26.754s passed
testLoadClosedGcdProofWithMergePointStatements() 7.060s passed
testLoadGcdProof() 6.485s passed
testLoadGcdProofWithPredAbstr() 6.859s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 6.448s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 6.319s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 5.388s passed
testMergeIndistinguishablePathConditionsWithITE() 5.635s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 5.707s passed

Standard output

873457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
873457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 496.5ns 
873473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
873676     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
873676     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
873676     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
873676     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
874426     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
880719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.25s 
880765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
880765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 
900228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
900228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 521.5ns 
900228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
906140     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.92s 
906203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
906533     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 330.57ms 
906533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
906533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 147.4ns 
906549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
912286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.73s 
912333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
912333     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.2ns 
923511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
923511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 174.8ns 
923511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
929272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.76s 
929319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
929944     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 544.74ms 
929944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
929944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 485.4ns 
929944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
935842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.9s 
935905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
936803     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 794.16ms 
936803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
936803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 184.2ns 
936803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
942479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.68s 
942510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
942510     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 466.6ns 
942510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
942510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.6ns 
942510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
947851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.33s 
947867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
947867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 331.3ns 
947898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
947898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 491.9ns 
947898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
953724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.83s 
953790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
954959     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07s 
954959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
954974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.3ms 
954974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
960563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.59s 
960594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
960594     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 378.1ns 
960594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
960594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 453.4ns 
960594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
966270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.67s 
966317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
966317     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16ns 
977707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
977707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 623.1ns 
977707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
983230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.52s 
983292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
984192     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 815.05ms