MergeRuleTests

11

tests

0

failures

0

ignored

1m8.57s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 11.628s passed
testDoAutomaticGcdProofWithMergePointStatements() 11.053s passed
testDoManualGcdProof() 19.314s passed
testLoadClosedGcdProofWithMergePointStatements() 3.957s passed
testLoadGcdProof() 3.708s passed
testLoadGcdProofWithPredAbstr() 3.897s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 3.540s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.110s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 2.678s passed
testMergeIndistinguishablePathConditionsWithITE() 2.909s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 2.780s passed

Standard output

442604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
442604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 820.2ns 
442604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442717     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
442717     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
442717     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
442717     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
443170     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
446406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.8s 
446453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
446453     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 
461913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
461913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 507.6ns 
461913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
464758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
465024     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 257.23ms 
465024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
465024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.4ns 
465024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
467981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
468012     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.5ns 
476652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
476652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.1ns 
476668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
479614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
480192     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 547.06ms 
480192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
480192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 406.7ns 
480192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
483299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
484089     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 755.04ms 
484089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
484089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.6ns 
484089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
486868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
486868     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 776.3ns 
486868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
486868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 379.1ns 
486883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
489533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
489533     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 528.2ns 
489564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
489564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 441.9ns 
489564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
492547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
493505     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 922.62ms 
493505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
493505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 462.8ns 
493521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
496420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
496420     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 526.1ns 
496420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
496420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 332.6ns 
496420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
499174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
499174     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.8ns 
507467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
507467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 463.3ns 
507467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
510413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
511175     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 718.5ms