MergeRuleTests

11

tests

0

failures

0

ignored

1m31.90s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 15.435s passed
testDoAutomaticGcdProofWithMergePointStatements() 14.959s passed
testDoManualGcdProof() 26.102s passed
testLoadClosedGcdProofWithMergePointStatements() 5.114s passed
testLoadGcdProof() 5.489s passed
testLoadGcdProofWithPredAbstr() 5.097s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.499s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.821s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.329s passed
testMergeIndistinguishablePathConditionsWithITE() 3.815s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 4.240s passed

Standard output

552417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
552417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.5ns 
552417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552546     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
552546     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
552546     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
552546     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
553140     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
557038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.62s 
557085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
557085     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 
578512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
578512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 503.6ns 
578528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 
581999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
582334     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 332.61ms 
582334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
582334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.7ns 
582350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 
585849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
585849     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.2ns 
597769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
597769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 520.8ns 
597769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.56s 
601382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
602268     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 843.74ms 
602268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
602268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 479.2ns 
602268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.78s 
606106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
607365     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19s 
607365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
607365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.9ns 
607381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.21s 
611605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
611605     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 897.2ns 
611605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
611605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144ns 
611620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
614903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
614919     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 683.2ns 
614934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
614934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 497.6ns 
614953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.7s 
618693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
620033     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29s 
620048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
620048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 588.1ns 
620048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
623816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.77s 
623847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
623847     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 720.7ns 
623878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
623878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.3ns 
623878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.61s 
627545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
627545     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.2ns 
638835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
638835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 625.9ns 
638851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.86s 
642775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
644245     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39s