aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2015-01-02 13:15:13 +0100
committerXavier Leroy <xavier.leroy@inria.fr>2015-01-02 13:15:13 +0100
commitce8f29b4b2502ce8c4da08dfea8796c49e2bc386 (patch)
tree3a59d41ecb99e64f29d8530dd0626720ce4226fa /cfrontend
parentd1104c07f7d79ac721c29774651ae512aacbcf3f (diff)
downloadcompcert-ce8f29b4b2502ce8c4da08dfea8796c49e2bc386.tar.gz
compcert-ce8f29b4b2502ce8c4da08dfea8796c49e2bc386.zip
PR#15: vararg functions are not eligible for inlining.
Diffstat (limited to 'cfrontend')
-rw-r--r--cfrontend/C2C.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index f3487acc..f9501439 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -954,7 +954,7 @@ let convertFundef loc env fd =
a_alignment = None;
a_sections = Sections.for_function env id' fd.fd_ret;
a_access = Sections.Access_default;
- a_inline = fd.fd_inline;
+ a_inline = fd.fd_inline && not fd.fd_vararg; (* PR#15 *)
a_loc = loc };
(id', Gfun(Internal {fn_return = ret;
fn_callconv = convertCallconv fd.fd_vararg fd.fd_attrib;