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 /backend/Inliningaux.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 'backend/Inliningaux.ml')
| -rw-r--r-- | backend/Inliningaux.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/backend/Inliningaux.ml b/backend/Inliningaux.ml index 42f58247..842e0c93 100644 --- a/backend/Inliningaux.ml +++ b/backend/Inliningaux.ml @@ -86,7 +86,10 @@ let static_called_once id io = (* To be considered: heuristics based on size of function? *) let should_inline (io: inlining_info) (id: ident) (f: coq_function) = - if !Clflags.option_finline && not (C2C.atom_is_noinline id) then - C2C.atom_is_inline id || static_called_once id io - else + if !Clflags.option_finline then begin + match C2C.atom_inline id with + | C2C.Inline -> true + | C2C.Noinline -> false + | C2C.No_specifier -> static_called_once id io + end else false |