MergeRuleTests

11

tests

0

failures

0

ignored

1m42.08s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 15.954s passed
testDoAutomaticGcdProofWithMergePointStatements() 15.478s passed
testDoManualGcdProof() 24.662s passed
testLoadClosedGcdProofWithMergePointStatements() 6.384s passed
testLoadGcdProof() 6.102s passed
testLoadGcdProofWithPredAbstr() 6.343s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 6.176s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 5.616s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 5.104s passed
testMergeIndistinguishablePathConditionsWithITE() 5.262s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 5.002s passed

Standard output

782988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
782988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 464.9ns 
782988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
783245     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
783245     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
783246     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
783246     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
783905     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
789471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.48s 
789518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
789518     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 
807646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
807646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 511.9ns 
807646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
812918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.26s 
812965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
813262     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 278.34ms 
813262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
813262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.1ns 
813262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
818485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.22s 
818532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
818547     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.7ns 
829232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
829232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 950.3ns 
829232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
834727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.49s 
834783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
835392     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 549.37ms 
835392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
835392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 467.9ns 
835392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
840784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.39s 
840846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
841733     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 791.73ms 
841737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
841738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 420ns 
841740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
846707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.97s 
846722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
846738     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 353.5ns 
846738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
846738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 378.8ns 
846738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
851776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.04s 
851807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
851807     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 256ns 
851842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
851842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 438.9ns 
851842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
857212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.36s 
857259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
858226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 881.11ms 
858226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
858226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.7ns 
858241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
863457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.23s 
863488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
863488     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 349.4ns 
863488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
863488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 324.3ns 
863488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
868651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.15s 
868698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
868698     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17ns 
878966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
878966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 520.6ns 
878966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
884177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.22s 
884240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
885068     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 748.45ms