MergeRuleTests

11

tests

0

failures

0

ignored

1m7.47s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 11.364s passed
testDoAutomaticGcdProofWithMergePointStatements() 11.105s passed
testDoManualGcdProof() 18.748s passed
testLoadClosedGcdProofWithMergePointStatements() 3.950s passed
testLoadGcdProof() 3.586s passed
testLoadGcdProofWithPredAbstr() 3.932s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 3.589s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.027s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 2.752s passed
testMergeIndistinguishablePathConditionsWithITE() 2.733s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 2.682s passed

Standard output

433145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
433145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 400.5ns 
433145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433256     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
433256     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
433256     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
433256     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
433679     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
436849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.7s 
436896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
436896     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 
451902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
451902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 445.7ns 
451902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
454711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
454929     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 225.95ms 
454929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
454929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 367ns 
454945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
457757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
457757     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.3ns 
466293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
466293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.4ns 
466293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
469316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
469867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 525.94ms 
469882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
469882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 408.9ns 
469882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
473030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
473814     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 736.06ms 
473814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
473814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 175.7ns 
473814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
476493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
476493     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 618.5ns 
476493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
476493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.7ns 
476493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
479233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
479233     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 508.4ns 
479248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
479248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 411.7ns 
479248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
482141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
483198     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01s 
483198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
483198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.3ns 
483198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
485916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
485931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
485931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 568.4ns 
485931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
485931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 421.6ns 
485931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
488714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
488714     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.3ns 
497037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
497037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 160.6ns 
497037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
499915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
500623     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 683.82ms