aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Inliningaux.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2017-12-07 15:01:20 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2017-12-07 15:01:20 +0100
commitd2efd8b0e1c07e8ce7edc2a5eaa461aff08d2be6 (patch)
tree1d998a607bd1afdcdbe9b055bf2e08ca382903ef /backend/Inliningaux.ml
parent3bb0c75456a0dcab079e7614c3bbd3ba971e4519 (diff)
downloadcompcert-kvx-d2efd8b0e1c07e8ce7edc2a5eaa461aff08d2be6.tar.gz
compcert-kvx-d2efd8b0e1c07e8ce7edc2a5eaa461aff08d2be6.zip
Do not inline varag functions. Bug 22642
Diffstat (limited to 'backend/Inliningaux.ml')
-rw-r--r--backend/Inliningaux.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/backend/Inliningaux.ml b/backend/Inliningaux.ml
index 164773ae..90a8c6c8 100644
--- a/backend/Inliningaux.ml
+++ b/backend/Inliningaux.ml
@@ -77,9 +77,9 @@ let inlining_analysis (p: program) =
empty_inlining_info
(* Test whether a function is static and called only once *)
-let static_called_once id io =
+let static_called_once fn_sig id io =
if !Clflags.option_finline_functions_called_once then
- C2C.atom_is_static id && call_count id io <= 1 && not (address_taken id io)
+ C2C.atom_is_static id && call_count id io <= 1 && not (address_taken id io) && not fn_sig.sig_cc.cc_vararg
else
false
@@ -87,6 +87,6 @@ let static_called_once id io =
let should_inline (io: inlining_info) (id: ident) (f: coq_function) =
if !Clflags.option_finline then
- C2C.atom_is_inline id || static_called_once id io
+ C2C.atom_is_inline id || static_called_once f.fn_sig id io
else
false