diff options
Diffstat (limited to 'cparser')
| -rw-r--r-- | cparser/C.mli | 3 | ||||
| -rw-r--r-- | cparser/Cprint.ml | 3 | ||||
| -rw-r--r-- | cparser/Cutil.ml | 2 | ||||
| -rw-r--r-- | cparser/Elab.ml | 5 | ||||
| -rw-r--r-- | cparser/Rename.ml | 1 |
5 files changed, 9 insertions, 5 deletions
diff --git a/cparser/C.mli b/cparser/C.mli index 5d90407..b1e44eb 100644 --- a/cparser/C.mli +++ b/cparser/C.mli @@ -231,7 +231,8 @@ type fundef = { fd_storage: storage; fd_inline: bool; fd_name: ident; - fd_ret: typ; (* return type *) + fd_attrib: attributes; + fd_ret: typ; (* return type *) fd_params: (ident * typ) list; (* formal parameters *) fd_vararg: bool; (* variable arguments? *) fd_locals: decl list; (* local variables *) diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml index c6864ff..0bbea68 100644 --- a/cparser/Cprint.ml +++ b/cparser/Cprint.ml @@ -458,7 +458,8 @@ let fundef pp f = fprintf pp "@[<hov 2>%s%a" (if f.fd_inline then "inline " else "") storage f.fd_storage; - simple_decl pp (f.fd_name, TFun(f.fd_ret, Some f.fd_params, f.fd_vararg, [])); + simple_decl pp (f.fd_name, + TFun(f.fd_ret, Some f.fd_params, f.fd_vararg, f.fd_attrib)); fprintf pp "@]@ @[<v 2>{@ "; List.iter (fun d -> fprintf pp "%a@ " full_decl d) f.fd_locals; stmt_block pp f.fd_body; diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 70ca8bc..ea4a905 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -453,7 +453,7 @@ let int_representable v nbits sgn = (* Type of a function definition *) let fundef_typ fd = - TFun(fd.fd_ret, Some fd.fd_params, fd.fd_vararg, []) + TFun(fd.fd_ret, Some fd.fd_params, fd.fd_vararg, fd.fd_attrib) (* Signedness of integer kinds *) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index d0e1b28..313569b 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1567,9 +1567,9 @@ let elab_fundef env (spec, name) body loc1 loc2 = | TFun(ty_ret, None, vararg, attr) -> TFun(ty_ret, Some [], vararg, attr) | _ -> ty in (* Extract info from type *) - let (ty_ret, params, vararg) = + let (ty_ret, params, vararg, attr) = match ty with - | TFun(ty_ret, Some params, vararg, attr) -> (ty_ret, params, vararg) + | TFun(ty_ret, Some params, vararg, attr) -> (ty_ret, params, vararg, attr) | _ -> fatal_error loc1 "wrong type for function definition" in (* Enter function in the environment, for recursive references *) let (fun_id, env1) = enter_or_refine_ident false loc1 env s sto ty in @@ -1584,6 +1584,7 @@ let elab_fundef env (spec, name) body loc1 loc2 = { fd_storage = sto; fd_inline = inline; fd_name = fun_id; + fd_attrib = attr; fd_ret = ty_ret; fd_params = params; fd_vararg = vararg; diff --git a/cparser/Rename.ml b/cparser/Rename.ml index 59b7bd7..f4bab8e 100644 --- a/cparser/Rename.ml +++ b/cparser/Rename.ml @@ -190,6 +190,7 @@ let fundef env f = ( { fd_storage = f.fd_storage; fd_inline = f.fd_inline; fd_name = name'; + fd_attrib = f.fd_attrib; fd_ret = typ env0 f.fd_ret; fd_params = params'; fd_vararg = f.fd_vararg; |