MergeRuleTests

11

tests

0

failures

0

ignored

1m38.88s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 15.348s passed
testDoAutomaticGcdProofWithMergePointStatements() 15.172s passed
testDoManualGcdProof() 23.965s passed
testLoadClosedGcdProofWithMergePointStatements() 6.703s passed
testLoadGcdProof() 5.965s passed
testLoadGcdProofWithPredAbstr() 5.856s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 5.636s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 5.326s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 4.927s passed
testMergeIndistinguishablePathConditionsWithITE() 4.853s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 5.127s passed

Standard output

770404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
770404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 510.2ns 
770404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
770576     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
770576     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
770576     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
770576     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
771248     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
776647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.25s 
776710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
776710     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 
794364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
794364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 169.9ns 
794379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
799373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.99s 
799420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
799690     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 270.45ms 
799706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
799706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.3ns 
799706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
804717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.01s 
804861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
804861     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.2ns 
815038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
815038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.5ns 
815038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
820078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.03s 
820125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
820674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 487.51ms 
820674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
820674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 471.3ns 
820690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
825712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.03s 
825758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
826514     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 662.16ms 
826530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
826530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141ns 
826530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
831626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.1s 
831642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
831657     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 437.4ns 
831657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
831657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.2ns 
831657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
836537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.87s 
836552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
836552     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 288.6ns 
836584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
836584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 472.8ns 
836584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
841814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.22s 
841878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
843274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3s 
843287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
843287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.5ns 
843287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
848109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.82s 
848124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
848124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 273ns 
848140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
848140     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.1ns 
848140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
853243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.11s 
853290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
853290     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.7ns 
863358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
863358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 834.5ns 
863358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
868495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.14s 
868542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
869277     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 629.98ms