diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-08 21:45:42 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-08 21:45:42 +0200 |
| commit | 63915fbebe707cc1de7c0ed5a24148cac45a742c (patch) | |
| tree | da503cba224f14281a2ee841930b8843459cb42b /common/Sections.ml | |
| parent | f78d61faf3db94ac1704ce0d11291211b5307629 (diff) | |
| parent | e326ed9f28a2ed6869f0cb356ef9a8e189cb0a47 (diff) | |
| download | compcert-kvx-63915fbebe707cc1de7c0ed5a24148cac45a742c.tar.gz compcert-kvx-63915fbebe707cc1de7c0ed5a24148cac45a742c.zip | |
Merge remote-tracking branch 'origin/mppa-work' into mppa-thread
Diffstat (limited to 'common/Sections.ml')
| -rw-r--r-- | common/Sections.ml | 29 |
1 files changed, 21 insertions, 8 deletions
diff --git a/common/Sections.ml b/common/Sections.ml index 9555c203..ea0b6dbc 100644 --- a/common/Sections.ml +++ b/common/Sections.ml @@ -166,9 +166,22 @@ let gcc_section name readonly exec = sec_writable = not readonly; sec_executable = exec; sec_access = Access_default } +(* Check and extract whether a section was given as attribute *) + +let get_attr_section loc attr = + match Cutil.find_custom_attributes ["section"; "__section__"] attr with + | [] -> None + | [[C.AString name]] -> Some name + | [[_]] -> + Diagnostics.error loc "'section' attribute requires a string"; + None + | _ -> + Diagnostics.error loc "ambiguous 'section' attribute"; + None + (* Determine section for a variable definition *) -let for_variable env id ty init thrl = +let for_variable env loc id ty init thrl = let attr = Cutil.attributes_of_type env ty in let readonly = List.mem C.AConst attr && not(List.mem C.AVolatile attr) in let si = @@ -176,11 +189,11 @@ let for_variable env id ty init thrl = (* 1- Section explicitly associated with #use_section *) Hashtbl.find use_section_table id with Not_found -> - match Cutil.find_custom_attributes ["section"; "__section__"] attr with - | [[C.AString name]] -> + match get_attr_section loc attr with + | Some name -> (* 2- Section given as an attribute, gcc-style *) gcc_section name readonly false - | _ -> + | None -> (* 3- Default section appropriate for size and const-ness *) let size = match Cutil.sizeof env ty with Some sz -> sz | None -> max_int in @@ -197,17 +210,17 @@ let for_variable env id ty init thrl = (* Determine sections for a function definition *) -let for_function env id attr = +let for_function env loc id attr = let si_code = try (* 1- Section explicitly associated with #use_section *) Hashtbl.find use_section_table id with Not_found -> - match Cutil.find_custom_attributes ["section"; "__section__"] attr with - | [[C.AString name]] -> + match get_attr_section loc attr with + | Some name -> (* 2- Section given as an attribute, gcc-style *) gcc_section name true true - | _ -> + | None -> (* 3- Default section *) try Hashtbl.find current_section_table "CODE" |