diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index be7ee677ba43a0c93425491803f9685c3c8138c8..084ea1a8202bb167ed68197be40e8a0d3cc1ac60 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -1386,10 +1386,16 @@ let findCompType ghost kind name tattr =
if kind = "enum" then
let enum, isnew = createEnumInfo name ~norig:name in
if isnew then
- cabsPushGlobal (GEnumTagDecl (enum, Current_loc.get ()));
+ begin
+ if not (Machine.gccMode ()) then
+ Kernel.error ~once:true
+ ~source:(fst @@ Current_loc.get ())
+ "forward declaration of enum %s" (Machdep.allowed_machdep "GCC");
+ cabsPushGlobal (GEnumTagDecl (enum, Current_loc.get ()));
+ end;
mk_tenum ~tattr enum
else
- let iss = if kind = "struct" then true else false in
+ let iss = kind = "struct" in
let self, isnew = createCompInfo iss name ~norig:name in
if isnew then
cabsPushGlobal (GCompTagDecl (self, Current_loc.get ()));
@@ -1418,8 +1424,8 @@ class canDropStmtClass pRes = object
method! vinst _ = Cil.SkipChildren
method! vexpr _ = Cil.SkipChildren
-
end
+
let canDropStatement (s: stmt) : bool =
let pRes = ref true in
let vis = new canDropStmtClass pRes in
@@ -6510,7 +6516,7 @@ and doExp local_env
| { tnode = TPtr t } -> begin
match unrollType t with
| { tnode = TFun (rt, at, isvar) } -> (* Make the function pointer
- * explicit *)
+ * explicit *)
let f'' =
match f'.enode with
| AddrOf lv -> new_exp ~loc:f'.eloc (Lval(lv))
@@ -9770,7 +9776,8 @@ and doTypedef ghost ((specs, nl): Cabs.name_group) =
Cil_datatype.Location.pretty oldloc
in
(* Tested with GCC+Clang: redefinition of compatible types in same scope:
- - enums are NOT allowed;
+ - enums are NOT allowed, except if they refer to the exact same
+ enumerated type
- composite types are allowed only if the composite type itself is
not redefined (complex rules; with some extra tag checking performed
in compatibleTypesp, we use tags here to detect redefinitions,
@@ -9798,8 +9805,29 @@ and doTypedef ghost ((specs, nl): Cabs.name_group) =
Kernel.fatal ~current:true "typeinfo.ttype (%a) should be TComp"
Cil_datatype.Typ.pretty typeinfo.ttype
end
- | TEnum _ -> (* GCC/Clang: "conflicting types" *)
- error_conflicting_types ()
+ | TEnum newei -> (* GCC/Clang: "conflicting types" *)
+ let t = unrollType typeinfo.ttype in
+ (match t.tnode with
+ | TEnum ei ->
+ if ei.ename <> newei.ename then
+ error_conflicting_types ()
+ else
+ warn_c11_redefinition ()
+ | TInt _ -> error_conflicting_types ()
+ | _ ->
+ Kernel.fatal
+ ~current:true "typeinfo.ttype (%a) should be an Enum"
+ Cil_datatype.Typ.pretty t)
+ | TInt _ ->
+ let t = unrollType typeinfo.ttype in
+ (match t.tnode with
+ | TInt _ -> warn_c11_redefinition ()
+ | TEnum _ -> error_conflicting_types ()
+ | _ ->
+ Kernel.fatal
+ ~current:true "typeinfo.ttype (%a) should be an int"
+ Cil_datatype.Typ.pretty t
+ )
| _ -> (* redeclaration in same scope valid only in C11 *)
warn_c11_redefinition ()
end
diff --git a/tests/syntax/ast_diff_1.i b/tests/syntax/ast_diff_1.i
index 86b0c7606e68395abec4be4f0e5f217d056450c7..4d93a93c5eaae6eca99f167bedf110ed48e44494 100644
--- a/tests/syntax/ast_diff_1.i
+++ b/tests/syntax/ast_diff_1.i
@@ -2,8 +2,8 @@
COMMENT: we need Eva for the loop unroll ACSL extension
PLUGIN: eva
MODULE: @PTEST_NAME@
- OPT: -then -ast-diff %{dep:ast_diff_2.c}
- OPT: -then -ast-diff %{dep:ast_diff_2.c} -cpp-extra-args="-DADD_ENUM_TAG"
+ OPT: -machdep gcc_x86_64 -then -ast-diff %{dep:ast_diff_2.c}
+ OPT: -machdep gcc_x86_64 -then -ast-diff %{dep:ast_diff_2.c} -cpp-extra-args="-DADD_ENUM_TAG"
*/
int X;
int Y=3;
diff --git a/tests/syntax/enum_forward.i b/tests/syntax/enum_forward.i
new file mode 100644
index 0000000000000000000000000000000000000000..6ae9fbdd9386d367b955bae2fb9f9de792c70b3f
--- /dev/null
+++ b/tests/syntax/enum_forward.i
@@ -0,0 +1,21 @@
+/* run.config
+ OPT: -machdep gcc_x86_64 -print
+ EXIT: 1
+ STDOPT:
+*/
+/* forward declaration of enum is supported by GCC but nonstandard */
+
+enum e X;
+enum e { V };
+
+enum g Y;
+typedef enum g { W } g;
+
+enum h;
+typedef enum h h;
+typedef enum h { Z } h;
+h hh = Z;
+
+typedef enum i { A } i;
+typedef enum i i;
+i ii = A;
diff --git a/tests/syntax/enum_redef_ko.i b/tests/syntax/enum_redef_ko.i
new file mode 100644
index 0000000000000000000000000000000000000000..d7358e0eceeb59fb30d06be5669994aa00b5eec6
--- /dev/null
+++ b/tests/syntax/enum_redef_ko.i
@@ -0,0 +1,9 @@
+/* run.config
+ EXIT: 1
+ STDOPT:
+*/
+
+/* redeclaration of enum */
+
+enum e { U };
+enum e { U };
diff --git a/tests/syntax/enum_redef_ok.i b/tests/syntax/enum_redef_ok.i
new file mode 100644
index 0000000000000000000000000000000000000000..bc488d4b192ed189f34e8289fa966466bee63e9d
--- /dev/null
+++ b/tests/syntax/enum_redef_ok.i
@@ -0,0 +1,9 @@
+/* run.config
+ STDOPT:
+*/
+
+/* "tentative definition" is allowed */
+
+enum e { U };
+enum e;
+enum e x = U;
diff --git a/tests/syntax/enum_typedef_redef.i b/tests/syntax/enum_typedef_redef.i
new file mode 100644
index 0000000000000000000000000000000000000000..2858e9f2778e1041a3c851b037ec596d277ff822
--- /dev/null
+++ b/tests/syntax/enum_typedef_redef.i
@@ -0,0 +1,19 @@
+/* run.config
+ EXIT: 1
+ STDOPT:
+*/
+
+/* this is the counterpart of enum_forward.i: we can accept a double typedef
+ with of an enum only if the first type is a forward declaration. */
+
+typedef enum h { Z } h;
+typedef enum h { Z } h;
+h hh = Z;
+
+// other problematic case, even though the enum is compatible with int
+
+typedef enum { E } t;
+typedef int t;
+
+typedef int q;
+typedef enum { F } q;
diff --git a/tests/syntax/oracle/enum_forward.0.res.oracle b/tests/syntax/oracle/enum_forward.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..c55d86c1ce477a053f345be172757f59f28ffd6a
--- /dev/null
+++ b/tests/syntax/oracle/enum_forward.0.res.oracle
@@ -0,0 +1,25 @@
+[kernel] Parsing enum_forward.i (no preprocessing)
+/* Generated by Frama-C */
+enum e;
+enum e {
+ V = 0
+};
+enum g;
+enum g {
+ W = 0
+};
+enum h;
+enum h;
+typedef enum h h;
+enum h {
+ Z = 0
+};
+enum i {
+ A = 0
+};
+typedef enum i i;
+enum e X;
+enum g Y;
+h hh = Z;
+i ii = A;
+
diff --git a/tests/syntax/oracle/enum_forward.1.res.oracle b/tests/syntax/oracle/enum_forward.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..30e3f01128fdd3df65d47b15337175297a729031
--- /dev/null
+++ b/tests/syntax/oracle/enum_forward.1.res.oracle
@@ -0,0 +1,9 @@
+[kernel] Parsing enum_forward.i (no preprocessing)
+[kernel] enum_forward.i:8: User Error:
+ forward declaration of enum only allowed for GCC machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
+[kernel] enum_forward.i:11: User Error:
+ forward declaration of enum only allowed for GCC machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
+[kernel] enum_forward.i:14: User Error:
+ forward declaration of enum only allowed for GCC machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
+[kernel] User Error: stopping on file "enum_forward.i" that has errors.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/enum_redef_ko.res.oracle b/tests/syntax/oracle/enum_redef_ko.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..93c3071d301a32de6b049ee62a9911f51300e439
--- /dev/null
+++ b/tests/syntax/oracle/enum_redef_ko.res.oracle
@@ -0,0 +1,9 @@
+[kernel] Parsing enum_redef_ko.i (no preprocessing)
+[kernel] enum_redef_ko.i:9: User Error:
+ redefinition of 'e' in the same scope.
+ Previous declaration was at enum_redef_ko.i:8
+[kernel] enum_redef_ko.i:9: User Error:
+ redefinition of 'U' in the same scope.
+ Previous declaration was at enum_redef_ko.i:8
+[kernel] User Error: stopping on file "enum_redef_ko.i" that has errors.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/enum_redef_ok.res.oracle b/tests/syntax/oracle/enum_redef_ok.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..c7df72848b6b4be8c95761feb7d2ba6959cf68af
--- /dev/null
+++ b/tests/syntax/oracle/enum_redef_ok.res.oracle
@@ -0,0 +1,8 @@
+[kernel] Parsing enum_redef_ok.i (no preprocessing)
+/* Generated by Frama-C */
+enum e {
+ U = 0
+};
+enum e;
+enum e x = U;
+
diff --git a/tests/syntax/oracle/enum_typedef_redef.res.oracle b/tests/syntax/oracle/enum_typedef_redef.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..75c247e34e14f5f1028fcd82ece255c02b046582
--- /dev/null
+++ b/tests/syntax/oracle/enum_typedef_redef.res.oracle
@@ -0,0 +1,18 @@
+[kernel] Parsing enum_typedef_redef.i (no preprocessing)
+[kernel] enum_typedef_redef.i:10: User Error:
+ redefinition of 'h' in the same scope.
+ Previous declaration was at enum_typedef_redef.i:9
+[kernel] enum_typedef_redef.i:10: User Error:
+ redefinition of 'Z' in the same scope.
+ Previous declaration was at enum_typedef_redef.i:9
+[kernel] enum_typedef_redef.i:10: User Error:
+ redefinition of type 'h' in the same scope with conflicting type.
+ Previous declaration was at enum_typedef_redef.i:9
+[kernel] enum_typedef_redef.i:16: User Error:
+ redefinition of type 't' in the same scope with conflicting type.
+ Previous declaration was at enum_typedef_redef.i:15
+[kernel] enum_typedef_redef.i:19: User Error:
+ redefinition of type 'q' in the same scope with conflicting type.
+ Previous declaration was at enum_typedef_redef.i:18
+[kernel] User Error: stopping on file "enum_typedef_redef.i" that has errors.
+[kernel] Frama-C aborted: invalid user input.