MergeRuleTests

11

tests

0

failures

0

ignored

1m6.77s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 11.110s passed
testDoAutomaticGcdProofWithMergePointStatements() 10.714s passed
testDoManualGcdProof() 18.913s passed
testLoadClosedGcdProofWithMergePointStatements() 3.747s passed
testLoadGcdProof() 3.522s passed
testLoadGcdProofWithPredAbstr() 3.872s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 3.524s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.081s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 2.770s passed
testMergeIndistinguishablePathConditionsWithITE() 2.838s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 2.678s passed

Standard output

429496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
429496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.5ns 
429496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429662     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
429662     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
429662     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
429662     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
430079     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
433161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.66s 
433193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
433193     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 
448431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
448431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.9ns 
448431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
451265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
451496     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 231.49ms 
451496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
451496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 362.2ns 
451512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
454345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
454345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.8ns 
462606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
462606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 477.6ns 
462606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
465568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
466131     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 545.62ms 
466131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
466131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.3ns 
466146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
469130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
470003     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 829.86ms 
470003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
470003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.1ns 
470018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
472681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
472681     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 613ns 
472697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
472697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.3ns 
472697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
475436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
475436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 485.9ns 
475452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
475467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 543ns 
475467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
478373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
479199     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 798.52ms 
479214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
479214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.2ns 
479214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
482044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
482044     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 496.8ns 
482044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
482044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 357.5ns 
482044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
484765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
484765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.8ns 
492751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
492751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 577.9ns 
492751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
495566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
496273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 675.01ms