Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit 442bffc9 authored by Sylvain Dailler's avatar Sylvain Dailler

ce bench: recover examples jlamp0

parent 3c35856d
......@@ -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
......
......@@ -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" ,
......
......@@ -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" ,
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment