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 8d336d5a authored by Sylvain Dailler's avatar Sylvain Dailler

ce: add test for assignment inside branches

parent 82189b35
module Test
use int.Int
use ref.Ref
val x : ref int
let f (a : int) : int
ensures { result = 0}
=
x := 42;
!x
let f2 (a : int) : int
ensures { result = 0}
=
x := 42;
!x
let f3 (a : int) : int
ensures { result = 0}
=
(if a = 0 then
x.contents <- 42
else
x := 18);
!x
let f4 (a : int) : int
ensures { result = 0}
=
(if a = 0 then
(x.contents <- 42; assert{ !x = 13})
else
(x := 18; assert { !x = 18}) );
17
end
Strongest Postcondition
bench/ce/if_assign.mlw Test VC f: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 10:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
bench/ce/if_assign.mlw Test VC f2: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 16:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
bench/ce/if_assign.mlw Test VC f3: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 21:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "0" }
Line 22:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
bench/ce/if_assign.mlw Test VC f3: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 21:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "-1" }
Line 22:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "18" }
bench/ce/if_assign.mlw Test VC f4: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 30:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "0" }
Line 34:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
bench/ce/if_assign.mlw Test VC f4: Valid
bench/ce/if_assign.mlw Test VC f4: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 30:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "-1" }
Line 31:
the check fails with all inputs
Weakest Precondition
bench/ce/if_assign.mlw Test VC f: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 10:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
Line 12:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
bench/ce/if_assign.mlw Test VC f2: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 16:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
Line 18:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
bench/ce/if_assign.mlw Test VC f3: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 21:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "0" }
Line 22:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
Line 25:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
bench/ce/if_assign.mlw Test VC f3: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 21:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "-1" }
Line 22:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "18" }
Line 27:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "18" }
bench/ce/if_assign.mlw Test VC f4: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 30:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "0" }
Line 34:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
bench/ce/if_assign.mlw Test VC f4: Valid
bench/ce/if_assign.mlw Test VC f4: Valid
bench/ce/if_assign.mlw Test VC f4: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 30:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "-1" }
Line 31:
the check fails with all inputs
Line 36:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "18" }
Strongest Postcondition
bench/ce/if_assign.mlw Test VC f: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 10:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
bench/ce/if_assign.mlw Test VC f2: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 16:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
bench/ce/if_assign.mlw Test VC f3: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 21:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "0" }
Line 22:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
bench/ce/if_assign.mlw Test VC f3: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 21:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "2" }
Line 22:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "18" }
bench/ce/if_assign.mlw Test VC f4: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 30:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "0" }
Line 34:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
bench/ce/if_assign.mlw Test VC f4: Valid
bench/ce/if_assign.mlw Test VC f4: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 30:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "2" }
Line 31:
the check fails with all inputs
Weakest Precondition
bench/ce/if_assign.mlw Test VC f: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 10:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
Line 12:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
bench/ce/if_assign.mlw Test VC f2: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 16:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
Line 18:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
bench/ce/if_assign.mlw Test VC f3: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 21:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "0" }
Line 22:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
Line 25:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
bench/ce/if_assign.mlw Test VC f3: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 21:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "2" }
Line 22:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "18" }
Line 27:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "18" }
bench/ce/if_assign.mlw Test VC f4: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 30:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "0" }
Line 34:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
bench/ce/if_assign.mlw Test VC f4: Valid
bench/ce/if_assign.mlw Test VC f4: Valid
bench/ce/if_assign.mlw Test VC f4: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 30:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "2" }
Line 31:
the check fails with all inputs
Line 36:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "18" }
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