aboutsummaryrefslogtreecommitdiffstats
path: root/extraction
diff options
context:
space:
mode:
authorBernhard Schommer <bschommer@users.noreply.github.com>2017-12-07 12:14:08 +0100
committerGitHub <noreply@github.com>2017-12-07 12:14:08 +0100
commit3bb0c75456a0dcab079e7614c3bbd3ba971e4519 (patch)
tree1dac031c6b94aafb7e28f63857dbdbe2f4870066 /extraction
parent90b76a0842b7f080893dd70a7c0c6bc878f4056b (diff)
downloadcompcert-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 'extraction')
-rw-r--r--extraction/extraction.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 247d6cfb..c5751e2b 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -76,6 +76,8 @@ Extraction Inline RTLgen.ret RTLgen.error RTLgen.bind RTLgen.bind2.
(* Inlining *)
Extract Inlined Constant Inlining.should_inline => "Inliningaux.should_inline".
+Extract Inlined Constant Inlining.inlining_info => "Inliningaux.inlining_info".
+Extract Inlined Constant Inlining.inlining_analysis => "Inliningaux.inlining_analysis".
Extraction Inline Inlining.ret Inlining.bind.
(* Allocation *)