MergeRuleTests

11

tests

0

failures

0

ignored

1m44.81s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 16.460s passed
testDoAutomaticGcdProofWithMergePointStatements() 16.007s passed
testDoManualGcdProof() 25.847s passed
testLoadClosedGcdProofWithMergePointStatements() 6.492s passed
testLoadGcdProof() 6.227s passed
testLoadGcdProofWithPredAbstr() 6.387s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 6.148s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 5.730s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 5.098s passed
testMergeIndistinguishablePathConditionsWithITE() 5.269s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 5.149s passed

Standard output

804951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
804951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 556.9ns 
804951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
805138     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
805138     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
805138     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
805138     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
806069     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
811770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.82s 
811848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
811848     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns 
830811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
830811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.6ns 
830811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
836163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.36s 
836210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
836525     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 305.81ms 
836525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
836525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.7ns 
836541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
842007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.47s 
842086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
842086     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.7ns 
852985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
852985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 180.9ns 
852985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
858497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.51s 
858562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
859118     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 505.24ms 
859133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
859133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 147.2ns 
859133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
864657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.52s 
864704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
865520     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 715.64ms 
865520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
865520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 272.2ns 
865520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
870637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.12s 
870669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
870669     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 367.6ns 
870669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
870669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.7ns 
870669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
875712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.04s 
875727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
875743     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 309.1ns 
875767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
875767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262ns 
875767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
881186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.42s 
881233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
882244     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 917.18ms 
882259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
882259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.4ns 
882275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
887496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.23s 
887528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
887528     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 277.4ns 
887528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
887528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 443.8ns 
887528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
892966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.44s 
893016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
893032     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.2ns 
903535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
903535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 174.5ns 
903551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
908694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.14s 
908788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
909762     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 860.41ms