MergeRuleTests

11

tests

0

failures

0

ignored

1m11.99s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 12.381s passed
testDoAutomaticGcdProofWithMergePointStatements() 12.146s passed
testDoManualGcdProof() 20.170s passed
testLoadClosedGcdProofWithMergePointStatements() 3.988s passed
testLoadGcdProof() 3.877s passed
testLoadGcdProofWithPredAbstr() 4.065s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 3.627s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.175s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 2.851s passed
testMergeIndistinguishablePathConditionsWithITE() 2.970s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 2.743s passed

Standard output

450030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
450030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.1ns 
450030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450155     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
450155     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
450155     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
450155     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
450624     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
453736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.7s 
453783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
453783     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 
470197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
470197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.1ns 
470197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
473106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
473372     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 255.1ms 
473372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
473372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 434.7ns 
473388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
476311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
476311     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.9ns 
485753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
485753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 165ns 
485753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
488754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
489364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 582.06ms 
489380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
489380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124ns 
489380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
492381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
493445     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02s 
493445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
493445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.1ns 
493461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
496196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
496196     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 888.6ns 
496196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
496196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.2ns 
496196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
499024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
499024     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 617.8ns 
499056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
499056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.1ns 
499056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
501980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
503012     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 996.96ms 
503028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
503028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 594.4ns 
503028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
505983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
505983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 647.2ns 
505998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
505998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.4ns 
505998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
508811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
508811     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.1ns 
518144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
518144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 483.4ns 
518144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
521051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
522021     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 814.76ms