MergeRuleTests

11

tests

0

failures

0

ignored

1m44.23s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 16.301s passed
testDoAutomaticGcdProofWithMergePointStatements() 15.675s passed
testDoManualGcdProof() 26.160s passed
testLoadClosedGcdProofWithMergePointStatements() 6.609s passed
testLoadGcdProof() 6.050s passed
testLoadGcdProofWithPredAbstr() 6.480s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 6.130s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 5.566s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 5.021s passed
testMergeIndistinguishablePathConditionsWithITE() 5.044s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 5.192s passed

Standard output

793637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
793637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 165ns 
793637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
793846     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
793846     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
793846     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
793846     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
794606     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
800182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.55s 
800245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
800245     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.6ns 
819794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
819794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 503.8ns 
819810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
825018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.21s 
825065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
825346     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 280.26ms 
825361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
825361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.5ns 
825361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
830578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.21s 
830619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
830635     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.6ns 
841662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
841662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 484ns 
841662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
847054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.38s 
847100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
847793     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 618.35ms 
847793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
847793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.8ns 
847793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
853211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.41s 
853274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
854273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 892.51ms 
854273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
854273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 208.3ns 
854273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
859434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.16s 
859450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
859465     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 394.1ns 
859465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
859465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.4ns 
859465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
864439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.97s 
864454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
864454     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 438.3ns 
864486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
864486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 452.4ns 
864501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
869888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.39s 
869934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
871095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06s 
871095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
871095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 153.6ns 
871095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
876108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.01s 
876124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
876139     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 339.3ns 
876139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
876139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 491.6ns 
876139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
881160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.02s 
881222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
881222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.1ns 
891814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
891814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 571.9ns 
891814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
896938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.11s 
896985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
897864     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 804.05ms