diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-04-07 14:02:15 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-04-07 14:08:33 +0200 |
| commit | 6cfc4dac7a8962bc49b88c9cb75156c7b6abd5c1 (patch) | |
| tree | 2e722cdf3c3153f1a22297c429a91c887bd63a6a /backend/PrintAsm.ml | |
| parent | 2086ba4770d435a084c65410ab061591e1a36c33 (diff) | |
| download | compcert-kvx-6cfc4dac7a8962bc49b88c9cb75156c7b6abd5c1.tar.gz compcert-kvx-6cfc4dac7a8962bc49b88c9cb75156c7b6abd5c1.zip | |
Do not generate code for "inline definitions"
ISO C99 states that "inline defintions", functions with inline
specifier that are not extern, does not provide an external
definition and another compilation unit can contain an external
definition. Thus in the case of non-static inline functions no
code should be generated.
Bug 21343
Diffstat (limited to 'backend/PrintAsm.ml')
| -rw-r--r-- | backend/PrintAsm.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml index 1f100b7e..0e9eadcb 100644 --- a/backend/PrintAsm.ml +++ b/backend/PrintAsm.ml @@ -102,7 +102,9 @@ module Printer(Target:TARGET) = let print_globdef oc (name,gdef) = match gdef with - | Gfun (Internal code) -> print_function oc name code + | Gfun (Internal code) -> + if not (C2C.atom_is_iso_inline_definition name) then + print_function oc name code | Gfun (External ef) -> () | Gvar v -> print_var oc name v |