MergeRuleTests

11

tests

0

failures

0

ignored

1m8.68s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 11.550s passed
testDoAutomaticGcdProofWithMergePointStatements() 11.180s passed
testDoManualGcdProof() 19.119s passed
testLoadClosedGcdProofWithMergePointStatements() 3.915s passed
testLoadGcdProof() 3.695s passed
testLoadGcdProofWithPredAbstr() 3.968s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 3.645s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.162s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 2.711s passed
testMergeIndistinguishablePathConditionsWithITE() 2.955s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 2.776s passed

Standard output

456893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
456893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 169.3ns 
456893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457008     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
457008     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
457008     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
457008     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
457545     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
460658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.75s 
460689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
460689     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 
476021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
476021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 483.4ns 
476021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
478931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
479183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 241.02ms 
479183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
479183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.1ns 
479183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
482061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
482061     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.7ns 
490733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
490733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 460.4ns 
490733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
493819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
494378     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 505.83ms 
494378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
494378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 385.9ns 
494378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
497565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
498346     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 736.76ms 
498346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
498346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 458.3ns 
498346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
501119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
501119     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 693ns 
501119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
501119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.53ms 
501119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
503818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
503818     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 572.4ns 
503833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
503833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 320.5ns 
503833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
506844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
507732     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 855.45ms 
507748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
507748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 162.4ns 
507748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
510688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
510704     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 510.8ns 
510704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
510704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.6ns 
510704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
513501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
513503     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.6ns 
521883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
521883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228ns 
521899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
524836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
525578     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 694.89ms