MergeRuleTests

11

tests

0

failures

0

ignored

1m46.15s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 16.166s passed
testDoAutomaticGcdProofWithMergePointStatements() 16.129s passed
testDoManualGcdProof() 26.650s passed
testLoadClosedGcdProofWithMergePointStatements() 6.805s passed
testLoadGcdProof() 6.522s passed
testLoadGcdProofWithPredAbstr() 6.641s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 6.640s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 5.702s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 5.041s passed
testMergeIndistinguishablePathConditionsWithITE() 5.014s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 4.835s passed

Standard output

812742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
812742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 631.4ns 
812742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
812945     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
812945     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
812945     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
812945     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
813759     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
819588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.85s 
819656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
819660     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 
839388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
839388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 487.2ns 
839388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
844575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.19s 
844715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
845091     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 358.78ms 
845091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
845091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 607.7ns 
845091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
850278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.18s 
850325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
850340     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.8ns 
861265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
861265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 588.5ns 
861265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
867023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.76s 
867069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
867898     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 751.97ms 
867898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
867898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 543.8ns 
867913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
873408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.51s 
873470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
874539     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 973.89ms 
874539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
874539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 428.6ns 
874539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
879359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.81s 
879374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
879374     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 415.1ns 
879374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
879374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139ns 
879390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
884369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.98s 
884384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
884400     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 332.4ns 
884431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
884431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 485ns 
884431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
889832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.41s 
889879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
891204     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24s 
891220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
891220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.04ms 
891220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
896203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.97s 
896218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
896218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 406.8ns 
896234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
896234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.6ns 
896234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
901305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.08s 
901368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
901368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.4ns 
912363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
912363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 512.5ns 
912363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
917855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.48s 
917902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
918885     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 884.57ms