MergeRuleTests

11

tests

0

failures

0

ignored

1m8.56s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 11.725s passed
testDoAutomaticGcdProofWithMergePointStatements() 11.437s passed
testDoManualGcdProof() 19.128s passed
testLoadClosedGcdProofWithMergePointStatements() 3.817s passed
testLoadGcdProof() 3.690s passed
testLoadGcdProofWithPredAbstr() 3.755s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 3.454s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.048s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 2.656s passed
testMergeIndistinguishablePathConditionsWithITE() 2.820s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.031s passed

Standard output

421129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
421129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.6ns 
421129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421254     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
421254     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
421254     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
421254     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
421754     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
424881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.75s 
424928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
424928     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 
440266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
440266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.1ns 
440266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
443017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
443299     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 278.61ms 
443314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
443314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.2ns 
443314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
446175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
446175     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.3ns 
455054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
455054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 392.5ns 
455054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
457900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
458494     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 569.12ms 
458494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
458494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 337.5ns 
458494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
461372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
462249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 825.45ms 
462249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
462249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 323.3ns 
462249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
465281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
465281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
465281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
465281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108ns 
465297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
467924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
467924     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 595.5ns 
467940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
467940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 264.9ns 
467955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
470785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
471754     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 920.64ms 
471754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
471754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.6ns 
471754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
474583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
474584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 619.1ns 
474584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
474584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 336.5ns 
474584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
477367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
477367     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.4ns 
486012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
486012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 526.5ns 
486012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
488890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
489687     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 763.11ms