MergeRuleTests

11

tests

0

failures

0

ignored

1m22.90s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 13.951s passed
testDoAutomaticGcdProofWithMergePointStatements() 14.196s passed
testDoManualGcdProof() 23.371s passed
testLoadClosedGcdProofWithMergePointStatements() 4.617s passed
testLoadGcdProof() 4.574s passed
testLoadGcdProofWithPredAbstr() 4.656s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.144s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.670s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.182s passed
testMergeIndistinguishablePathConditionsWithITE() 3.378s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.164s passed

Standard output

556134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
556134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 716.5ns 
556134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556272     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
556272     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
556272     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
556272     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
556803     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
560648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.51s 
560696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
560696     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 
579500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
579500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 470.9ns 
579500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
582889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
583170     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 278.66ms 
583170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
583170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 379.1ns 
583186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 
586685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
586685     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.3ns 
597121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
597121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.8ns 
597121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
600485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
601265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 736.93ms 
601265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
601265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 406.1ns 
601265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.5s 
604825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
605921     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05s 
605921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
605921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 190.9ns 
605921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
609085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
609085     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 799.7ns 
609085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
609085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.5ns 
609085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
612236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
612236     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 585.8ns 
612267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
612267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 301ns 
612267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
615634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
616884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08s 
616884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
616884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 204ns 
616900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
620262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
620262     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 521.1ns 
620262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
620262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 453.7ns 
620278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
623520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
623567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
623567     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.7ns 
634458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
634458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 450.2ns 
634458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.5s 
638003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
639032     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 992.54ms