diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2017-12-07 12:14:08 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-12-07 12:14:08 +0100 |
| commit | 3bb0c75456a0dcab079e7614c3bbd3ba971e4519 (patch) | |
| tree | 1dac031c6b94aafb7e28f63857dbdbe2f4870066 /driver/Clflags.ml | |
| parent | 90b76a0842b7f080893dd70a7c0c6bc878f4056b (diff) | |
| download | compcert-3bb0c75456a0dcab079e7614c3bbd3ba971e4519.tar.gz compcert-3bb0c75456a0dcab079e7614c3bbd3ba971e4519.zip | |
Inlining of static functions which are only called once. (#37)
New inlining heuristic for static functions.
Static functions that are only called once can always be inlined,
since they can be removed safely after inlining and no call
prologue, epilogue, as well as register saving and needs to be
generated.
Diffstat (limited to 'driver/Clflags.ml')
| -rw-r--r-- | driver/Clflags.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 2d92e09b..a886ee9b 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -34,6 +34,7 @@ let option_finline_asm = ref false let option_mthumb = ref (Configuration.model = "armv7m") let option_Osize = ref false let option_finline = ref true +let option_finline_functions_called_once = ref true let option_dprepro = ref false let option_dparse = ref false let option_dcmedium = ref false |