MergeRuleTests

11

tests

0

failures

0

ignored

1m26.76s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 15.235s passed
testDoAutomaticGcdProofWithMergePointStatements() 13.922s passed
testDoManualGcdProof() 24.837s passed
testLoadClosedGcdProofWithMergePointStatements() 4.809s passed
testLoadGcdProof() 5.116s passed
testLoadGcdProofWithPredAbstr() 4.971s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.079s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.746s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.190s passed
testMergeIndistinguishablePathConditionsWithITE() 3.369s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.483s passed

Standard output

540241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
540241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 202.8ns 
540241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540377     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
540377     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
540377     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
540377     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
540912     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
544757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.52s 
544820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
544820     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.1ns 
565071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
565071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 296.8ns 
565071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
568514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
568817     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 288.58ms 
568817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
568817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.6ns 
568817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
572231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
572247     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ms 
584052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
584052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.8ns 
584068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
587478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
588131     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 615.4ms 
588131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
588131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.1ns 
588131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 
591656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
593053     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34s 
593102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
593102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.5ns 
593102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 
596585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
596585     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 753.4ns 
596585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
596585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.5ns 
596601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
599759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
599759     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 554.9ns 
599790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
599790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.5ns 
599790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
603160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
604584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38s 
604584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
604584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 462.6ns 
604584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
607953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
607953     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 563.1ns 
607953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
607953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 160.6ns 
607953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
611265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
611265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.2ns 
621875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
621875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 208.5ns 
621891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
626004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.12s 
626050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
626991     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 854.58ms