From abb6fbfe333173acfeeb9304f9c529778e58ff1c Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 16 Apr 2011 08:20:45 +0000 Subject: Preliminary support for 'aligned' and 'section' attributes, gcc-style. New-style handling of sections for IA32 and ARM. Work in progress, to be tested. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1635 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/C2C.ml | 37 +++++++++++++++---------------------- 1 file changed, 15 insertions(+), 22 deletions(-) (limited to 'cfrontend/C2C.ml') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 966bb76b..1a6539ac 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -719,7 +719,7 @@ let convertFundef env fd = a_env = env; a_type = Cutil.fundef_typ fd; a_fundef = Some fd }; - Sections.define_function id'; + Sections.define_function env id' fd.fd_ret; Datatypes.Coq_pair(id', Internal {fn_return = ret; fn_params = params; fn_vars = vars; fn_body = body'}) @@ -776,21 +776,6 @@ let convertInitializer env ty i = (** Global variable *) -let rec type_is_readonly env t = - let a = Cutil.attributes_of_type env t in - if List.mem C.AVolatile a then false else - if List.mem C.AConst a then true else - match Cutil.unroll env t with - | C.TArray(t', _, _) -> type_is_readonly env t' - | _ -> false - -let rec type_is_volatile env t = - let a = Cutil.attributes_of_type env t in - if List.mem C.AConst a then true else - match Cutil.unroll env t with - | C.TArray(t', _, _) -> type_is_volatile env t' - | _ -> false - let convertGlobvar env (sto, id, ty, optinit) = let id' = intern_string id.name in let ty' = convertTyp env ty in @@ -805,13 +790,14 @@ let convertGlobvar env (sto, id, ty, optinit) = a_env = env; a_type = ty; a_fundef = None }; - Sections.define_variable id' - (match Cutil.sizeof env ty with Some sz -> sz | None -> max_int) - (type_is_readonly env ty); + Sections.define_variable env id' ty; + let a = Cutil.attributes_of_type env ty in + let volatile = List.mem C.AVolatile a in + let readonly = List.mem C.AConst a && not volatile in Datatypes.Coq_pair(id', {gvar_info = ty'; gvar_init = init'; - gvar_readonly = type_is_readonly env ty; - gvar_volatile = type_is_volatile env ty}) + gvar_readonly = readonly; + gvar_volatile = volatile}) (** Convert a list of global declarations. Result is a pair [(funs, vars)] where [funs] are @@ -937,6 +923,7 @@ let atom_is_extern a = with Not_found -> false +(* let atom_is_readonly a = try let i = Hashtbl.find decl_atom a in type_is_readonly i.a_env i.a_type @@ -948,10 +935,16 @@ let atom_sizeof a = let i = Hashtbl.find decl_atom a in Cutil.sizeof i.a_env i.a_type with Not_found -> None +*) let atom_alignof a = try - let i = Hashtbl.find decl_atom a in Cutil.alignof i.a_env i.a_type + let i = Hashtbl.find decl_atom a in + match Cutil.find_custom_attributes + ["aligned"; "__aligned__"] + (Cutil.attributes_of_type i.a_env i.a_type) with + | [[C.AInt n]] -> Some(Int64.to_int n) + | _ -> Cutil.alignof i.a_env i.a_type with Not_found -> None -- cgit