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 1f45ff36 authored by Cláudio Belo Lourenço's avatar Cláudio Belo Lourenço

Documentation about the introduction of attributes in the API

parent a28e2c96
......@@ -28,7 +28,7 @@ let env : Env.env = Env.create_env (Whyconf.loadpath main)
declaration of
BEGIN{source2}
let f2 () : int
let f2 [@foo] () : int
requires { true }
ensures { result >= 0 }
= let x = ref 42 in !x
......@@ -63,7 +63,8 @@ let get_fun : Expr.rsymbol =
(* BEGIN{code2} *)
let d2 =
let id = Ident.id_fresh "f" in
let attrs = Ident.(Sattr.singleton (create_attribute "foo")) in
let id = Ident.id_fresh ~attrs "f" in
let post =
let result =
Term.create_vsymbol (Ident.id_fresh "result") Ty.ty_int
......
......@@ -96,7 +96,7 @@ let mod_M1 =
(* declaration of
BEGIN{source2}
module M2
let f (x:int) : int
let f [@foo] (x:int) : int
requires { x=6 }
ensures { result=42 }
= x*7
......@@ -137,7 +137,9 @@ let mod_M2 =
Efun(param1 id_x int_type, None, mk_pat Pwild,
Ity.MaskVisible, spec, body)
in
Dlet(mk_ident "f",false,Expr.RKnone, mk_expr f)
let attr = ATstr (Ident.create_attribute "foo") in
let id = { (mk_ident "f") with id_ats = [attr] } in
Dlet(id,false,Expr.RKnone, mk_expr f)
in
(mk_ident "M2",[use_int_Int ; f])
(* END{code2} *)
......
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