Documentation about the introduction of attributes in the API

parent 0de3e3b8
......@@ -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