summaryrefslogtreecommitdiff
path: root/cparser/Elab.ml
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-05-12 08:20:14 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-05-12 08:20:14 +0000
commit951bf7bdb208f500c86e8d45c45247cd25adb4ab (patch)
tree164a59b4eba4f1ede5ec37bc357b4d7238eb3828 /cparser/Elab.ml
parent3a9359e3d89f41d8003b1ea4e01254bb38ea534d (diff)
Incorrect conversion of K&R functions. Example of problem:
void * foo(s, u) ... git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2491 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cparser/Elab.ml')
-rw-r--r--cparser/Elab.ml5
1 files changed, 3 insertions, 2 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index f4b2061..542ee18 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -1878,7 +1878,7 @@ let elab_fundef env spec name body loc =
env1
let elab_kr_fundef env spec name params defs body loc =
- warning loc "Non-prototype, pre-standard function definition.@ Converting to prototype form.";
+ warning loc "Non-prototype, pre-standard function definition.@ Converting to prototype form";
(* Check that the declarations only declare parameters *)
let check_one_decl (Init_name(Name(s, dty, attrs, loc'), ie)) =
if not (List.mem s params) then
@@ -1914,7 +1914,8 @@ let elab_kr_fundef env spec name params defs body loc =
List.map (fun p -> convert_param p defs) params in
let name' =
let (Name(s, dty, attr, loc')) = name in
- Name(s, PROTO(dty, (params', false)), attr, loc') in
+ Name(s, append_decltype dty (PROTO(JUSTBASE, (params', false))),
+ attr, loc') in
(* Elaborate the prototyped form *)
elab_fundef env spec name' body loc