aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2014-11-26 15:50:36 +0100
committerXavier Leroy <xavier.leroy@inria.fr>2014-11-26 15:50:36 +0100
commitc3b615f875ed2cf8418453c79c4621d2dc61b0a0 (patch)
tree8e125450f2313e35d36618ac8c1dfca62688afc3
parent1ccc058794381d7d7c2ff704786009019489001d (diff)
downloadcompcert-c3b615f875ed2cf8418453c79c4621d2dc61b0a0.tar.gz
compcert-c3b615f875ed2cf8418453c79c4621d2dc61b0a0.zip
Wrong handling of block-local function declarations (in Elab.ml).
-rw-r--r--cparser/Elab.ml19
-rw-r--r--test/regression/Makefile3
-rw-r--r--test/regression/Results/decl11
-rw-r--r--test/regression/decl1.c21
4 files changed, 31 insertions, 13 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index c4057e63..43a72a0e 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -1770,18 +1770,13 @@ let enter_decdefs local loc env sto dl =
if sto <> Storage_default && dl = [] then
warning loc "Storage class specifier on empty declaration";
let rec enter_decdef (decls, env) (s, ty, init) =
+ let isfun = is_function_type env ty in
if sto = Storage_extern && init <> NO_INIT then
error loc "'extern' declaration cannot have an initializer";
- (* Adjust storage for function declarations *)
- let sto1 =
- match unroll env ty, sto with
- | TFun _, Storage_default ->
- Storage_extern
- | TFun _, (Storage_static | Storage_register) ->
- if local then error loc "invalid storage class for '%s'" s;
- sto
- | _, _ ->
- sto in
+ if local && isfun && (sto = Storage_static || sto = Storage_register) then
+ error loc "invalid storage class for '%s'" s;
+ (* Local function declarations are always treated as extern *)
+ let sto1 = if local && isfun then Storage_extern else sto in
(* enter ident in environment with declared type, because
initializer can refer to the ident *)
let (id, sto', env1) = enter_or_refine_ident local loc env s sto1 ty in
@@ -1791,10 +1786,10 @@ let enter_decdefs local loc env sto dl =
let env2 = Env.add_ident env1 id sto' ty' in
(* check for incomplete type *)
if local && sto' <> Storage_extern
- && not (is_function_type env ty')
+ && not isfun
&& wrap incomplete_type loc env ty' then
error loc "'%s' has incomplete type" s;
- if local && sto' <> Storage_extern && sto' <> Storage_static then
+ if local && not isfun && sto' <> Storage_extern && sto' <> Storage_static then
(* Local definition *)
((sto', id, ty', init') :: decls, env2)
else begin
diff --git a/test/regression/Makefile b/test/regression/Makefile
index f4f96233..5c601211 100644
--- a/test/regression/Makefile
+++ b/test/regression/Makefile
@@ -16,7 +16,8 @@ TESTS=int32 int64 floats floats-basics \
expr1 expr6 funptr2 initializers initializers2 initializers3 \
volatile1 volatile2 volatile3 \
funct3 expr5 struct7 struct8 struct11 casts1 casts2 char1 \
- sizeof1 sizeof2 binops bool for1 switch switch2 compound
+ sizeof1 sizeof2 binops bool for1 switch switch2 compound \
+ decl1
# Can run, but only in compiled mode, and have reference output in Results
diff --git a/test/regression/Results/decl1 b/test/regression/Results/decl1
new file mode 100644
index 00000000..fa8248b0
--- /dev/null
+++ b/test/regression/Results/decl1
@@ -0,0 +1 @@
+Result is 2
diff --git a/test/regression/decl1.c b/test/regression/decl1.c
new file mode 100644
index 00000000..d2aedba7
--- /dev/null
+++ b/test/regression/decl1.c
@@ -0,0 +1,21 @@
+#include <stdio.h>
+
+/* Local function declarations */
+
+int f (int p)
+{
+ p = p + 1;
+ return p;
+}
+
+int main (int argc, char **argv)
+{
+ int (*p)();
+ int f();
+ int i;
+
+ p = f;
+ i = (*p)(1);
+ printf("Result is %d\n", i);
+ return 0;
+}