From 442bffc9b7acdfa9b579c4103a5f86160095566a Mon Sep 17 00:00:00 2001 From: Sylvain Dailler <dailler@adacore.com> Date: Tue, 18 Sep 2018 10:50:23 +0200 Subject: [PATCH] ce bench: recover examples jlamp0 --- bench/ce/jlamp0.mlw | 7 ++-- bench/ce/jlamp0_CVC4,1.5.oracle | 73 ++++++++++++++++++++++++--------- bench/ce/jlamp0_Z3,4.6.0.oracle | 73 ++++++++++++++++++++++++--------- 3 files changed, 109 insertions(+), 44 deletions(-) diff --git a/bench/ce/jlamp0.mlw b/bench/ce/jlamp0.mlw index 40d952593..8be63b303 100644 --- a/bench/ce/jlamp0.mlw +++ b/bench/ce/jlamp0.mlw @@ -8,10 +8,9 @@ module M let p1 (b : ref int) requires { 0 <= !a <= 10 /\ 3 <= !b <= 17 } ensures { 17 <= !a <= 42 } - = - a.contents <- !a + !b; - (*assert { 5 <= !a <= 15 };*) - (*if !a >= 10 then a.contents <- !a - 1*) () + = a := !a + !b; + assert { 5 <= !a <= 15 }; + if !a >= 10 then a := !a - 1 val c : ref int diff --git a/bench/ce/jlamp0_CVC4,1.5.oracle b/bench/ce/jlamp0_CVC4,1.5.oracle index 53d42ca66..65bb36176 100644 --- a/bench/ce/jlamp0_CVC4,1.5.oracle +++ b/bench/ce/jlamp0_CVC4,1.5.oracle @@ -6,22 +6,55 @@ a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , Line 8: b, [[@introduced], [@model_trace:b]] = {"type" : "Integer" , "val" : "3" } -Line 10: +Line 11: a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , "val" : "3" } Line 12: a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , "val" : "3" } +bench/ce/jlamp0.mlw M VC p1: Unknown (unknown) +Counter-example model:File jlamp0.mlw: +Line 6: +a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , +"val" : "7" } +Line 8: +b, [[@introduced], [@model_trace:b]] = {"type" : "Integer" , +"val" : "3" } +Line 10: +a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , +"val" : "9" } +Line 11: +a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , +"val" : "10" } +Line 13: +a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , +"val" : "9" } + +bench/ce/jlamp0.mlw M VC p1: Unknown (unknown) +Counter-example model:File jlamp0.mlw: +Line 6: +a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , +"val" : "2" } +Line 8: +b, [[@introduced], [@model_trace:b]] = {"type" : "Integer" , +"val" : "3" } +Line 10: +a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , +"val" : "5" } +Line 11: +a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , +"val" : "5" } + bench/ce/jlamp0.mlw M VC p2: Unknown (unknown) Counter-example model:File jlamp0.mlw: Line 6: a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , "val" : "0" } -Line 21: +Line 20: c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" , "val" : "1" } -Line 23: +Line 22: c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" , "val" : "1" } @@ -31,20 +64,20 @@ Counter-example model:File jlamp0.mlw: Line 6: a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , "val" : "0" } -Line 21: +Line 20: c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" , "val" : "1" } -Line 22: +Line 21: a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , "val" : "3" } c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" , "val" : "2" } c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" , "val" : "4" } -Line 26: +Line 25: a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , "val" : "5" } -Line 27: +Line 26: c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" , "val" : "4" } @@ -53,21 +86,21 @@ Counter-example model:File jlamp0.mlw: Line 6: a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , "val" : "0" } -Line 21: +Line 20: c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" , "val" : "1" } -Line 22: +Line 21: a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , "val" : "3" } c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" , "val" : "10" } -Line 23: +Line 22: c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" , "val" : "12" } -Line 26: +Line 25: a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , "val" : "13" } -Line 27: +Line 26: c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" , "val" : "12" } @@ -76,21 +109,21 @@ Counter-example model:File jlamp0.mlw: Line 6: a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , "val" : "0" } -Line 21: +Line 20: c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" , "val" : "1" } -Line 22: +Line 21: a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , "val" : "9" } c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" , "val" : "2" } -Line 24: +Line 23: a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , "val" : "11" } -Line 26: +Line 25: a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , "val" : "11" } -Line 27: +Line 26: c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" , "val" : "4" } @@ -99,13 +132,13 @@ Counter-example model:File jlamp0.mlw: Line 6: a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , "val" : "0" } -Line 20: +Line 19: a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , "val" : "3" } -Line 21: +Line 20: c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" , "val" : "1" } -Line 22: +Line 21: a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , "val" : "3" } c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" , diff --git a/bench/ce/jlamp0_Z3,4.6.0.oracle b/bench/ce/jlamp0_Z3,4.6.0.oracle index 06c5aaddf..b9d6e8973 100644 --- a/bench/ce/jlamp0_Z3,4.6.0.oracle +++ b/bench/ce/jlamp0_Z3,4.6.0.oracle @@ -6,22 +6,55 @@ a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , Line 8: b, [[@introduced], [@model_trace:b]] = {"type" : "Integer" , "val" : "3" } -Line 10: +Line 11: a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , "val" : "3" } Line 12: a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , "val" : "3" } +bench/ce/jlamp0.mlw M VC p1: Timeout +Counter-example model:File jlamp0.mlw: +Line 6: +a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , +"val" : "7" } +Line 8: +b, [[@introduced], [@model_trace:b]] = {"type" : "Integer" , +"val" : "3" } +Line 10: +a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , +"val" : "9" } +Line 11: +a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , +"val" : "10" } +Line 13: +a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , +"val" : "9" } + +bench/ce/jlamp0.mlw M VC p1: Timeout +Counter-example model:File jlamp0.mlw: +Line 6: +a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , +"val" : "2" } +Line 8: +b, [[@introduced], [@model_trace:b]] = {"type" : "Integer" , +"val" : "3" } +Line 10: +a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , +"val" : "5" } +Line 11: +a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , +"val" : "5" } + bench/ce/jlamp0.mlw M VC p2: Timeout Counter-example model:File jlamp0.mlw: Line 6: a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , "val" : "0" } -Line 21: +Line 20: c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" , "val" : "1" } -Line 23: +Line 22: c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" , "val" : "1" } @@ -31,20 +64,20 @@ Counter-example model:File jlamp0.mlw: Line 6: a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , "val" : "0" } -Line 21: +Line 20: c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" , "val" : "1" } -Line 22: +Line 21: a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , "val" : "3" } c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" , "val" : "2" } c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" , "val" : "4" } -Line 26: +Line 25: a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , "val" : "5" } -Line 27: +Line 26: c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" , "val" : "4" } @@ -53,21 +86,21 @@ Counter-example model:File jlamp0.mlw: Line 6: a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , "val" : "0" } -Line 21: +Line 20: c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" , "val" : "1" } -Line 22: +Line 21: a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , "val" : "3" } c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" , "val" : "10" } -Line 23: +Line 22: c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" , "val" : "12" } -Line 26: +Line 25: a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , "val" : "13" } -Line 27: +Line 26: c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" , "val" : "12" } @@ -76,21 +109,21 @@ Counter-example model:File jlamp0.mlw: Line 6: a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , "val" : "0" } -Line 21: +Line 20: c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" , "val" : "1" } -Line 22: +Line 21: a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , "val" : "9" } c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" , "val" : "2" } -Line 24: +Line 23: a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , "val" : "11" } -Line 26: +Line 25: a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , "val" : "11" } -Line 27: +Line 26: c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" , "val" : "4" } @@ -99,13 +132,13 @@ Counter-example model:File jlamp0.mlw: Line 6: a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , "val" : "0" } -Line 20: +Line 19: a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , "val" : "3" } -Line 21: +Line 20: c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" , "val" : "1" } -Line 22: +Line 21: a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" , "val" : "3" } c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" , -- GitLab