MergeRuleTests

11

tests

0

failures

0

ignored

1m22.17s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 14.014s passed
testDoAutomaticGcdProofWithMergePointStatements() 13.960s passed
testDoManualGcdProof() 23.708s passed
testLoadClosedGcdProofWithMergePointStatements() 4.647s passed
testLoadGcdProof() 4.379s passed
testLoadGcdProofWithPredAbstr() 4.823s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.121s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.455s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 2.921s passed
testMergeIndistinguishablePathConditionsWithITE() 3.151s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 2.992s passed

Standard output

513345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
513345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.7ns 
513345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513479     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
513479     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
513479     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
513479     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
514014     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
517674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.33s 
517733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
517736     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 
537075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
537075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 427.5ns 
537075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
540204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
540516     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 308.59ms 
540532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
540532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 162.5ns 
540532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.58s 
544167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
544167     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.1ns 
554530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
554530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.4ns 
554530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
557947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
558651     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 670.61ms 
558651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
558651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 375.8ns 
558651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.71s 
562410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
563474     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02s 
563474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
563474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 176.5ns 
563489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
566462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
566477     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 733.6ns 
566477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
566477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 368.8ns 
566477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
569353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
569353     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 774.5ns 
569389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
569390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.2ns 
569391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.47s 
572911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
574019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08s 
574035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
574035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.15ms 
574035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
577186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
577186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 608.8ns 
577186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
577186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 414.6ns 
577202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
580364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
580364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.2ns 
591146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
591146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 308.8ns 
591146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
594488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
595525     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1s