diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-12-08 16:24:49 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bschommer@users.noreply.github.com> | 2017-12-08 16:31:58 +0100 |
| commit | 35db979d7e723ba2ac5bef4629a15b4919d937d4 (patch) | |
| tree | 2f34bae6f8a6f1d4c66579bf23190010b9949ac9 /cfrontend/C2C.ml | |
| parent | f05e9e7ee26116ab88d8a5d7ff3ea68d1bd950ca (diff) | |
| download | compcert-kvx-35db979d7e723ba2ac5bef4629a15b4919d937d4.tar.gz compcert-kvx-35db979d7e723ba2ac5bef4629a15b4919d937d4.zip | |
Introduce and use C2C.atom_inline function with 3-valued result
Instead of two Boolean tests C2C.atom_is_{no,}inline, have a single
C2C.atom_inline function that returns one of the three possible values
stored in the the a_inline field.
Diffstat (limited to 'cfrontend/C2C.ml')
| -rw-r--r-- | cfrontend/C2C.ml | 16 |
1 files changed, 5 insertions, 11 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index bbeda741..2b3b50bf 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -26,7 +26,7 @@ open Csyntax (** Record useful information about global variables and functions, and associate it with the corresponding atoms. *) -type atom_inline = +type inline_status = | No_specifier (* No inline specifier and no noinline attribute *) | Noinline (* The atom is declared with the noinline attribute *) | Inline (* The atom is declared inline *) @@ -37,7 +37,7 @@ type atom_info = a_sections: Sections.section_name list; (* in which section to put it *) (* 1 section for data, 3 sections (code/lit/jumptbl) for functions *) a_access: Sections.access_mode; (* access mode, e.g. small data area *) - a_inline: atom_inline; (* function declared inline? *) + a_inline: inline_status; (* function declared inline? *) a_loc: location (* source location *) } @@ -79,17 +79,11 @@ let atom_is_rel_data a ofs = with Not_found -> false -let atom_is_inline a = +let atom_inline a = try - (Hashtbl.find decl_atom a).a_inline = Inline + (Hashtbl.find decl_atom a).a_inline with Not_found -> - false - -let atom_is_noinline a = - try - (Hashtbl.find decl_atom a).a_inline = Noinline - with Not_found -> - false + No_specifier (** Iso C99 defines inline definitions of functions as functions with inline specifier and without extern. These functions do |