MergeRuleTests

11

tests

0

failures

0

ignored

1m58.97s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 19.825s passed
testDoAutomaticGcdProofWithMergePointStatements() 18.293s passed
testDoManualGcdProof() 32.162s passed
testLoadClosedGcdProofWithMergePointStatements() 6.910s passed
testLoadGcdProof() 6.802s passed
testLoadGcdProofWithPredAbstr() 6.785s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 6.505s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 5.849s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 5.082s passed
testMergeIndistinguishablePathConditionsWithITE() 5.270s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 5.488s passed

Standard output

804166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
804166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 539.4ns 
804166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
804385     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
804385     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
804385     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
804385     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
805354     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
811123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.96s 
811186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
811186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 
836341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
836341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.2ns 
836341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
841689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.35s 
841767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
842175     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 400.88ms 
842175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
842175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.6ns 
842175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
847647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.47s 
847725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
847741     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25ns 
862000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
862000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 334ns 
862000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
867410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.41s 
867488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
868489     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 939.6ms 
868505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
868505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 277.8ns 
868505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
873992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.48s 
874039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
875290     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14s 
875290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
875290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 326.3ns 
875305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
880747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.45s 
880778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
880778     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 791.7ns 
880778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
880778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.7ns 
880798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
885813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.02s 
885829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
885844     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 561.5ns 
885876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
885876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.8ns 
885876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
891285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.41s 
891347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
892755     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33s 
892770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
892770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 502.8ns 
892786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
898009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.23s 
898040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
898040     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 392.9ns 
898040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
898040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.6ns 
898040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
903215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.17s 
903262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
903278     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.2ns 
916333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
916333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 316.2ns 
916349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
921760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.42s 
921823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
923135     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22s