From b09129b4d8d397824574d9e955e5729734007d84 Mon Sep 17 00:00:00 2001
From: christophe <christophe.junke@cea.fr>
Date: Tue, 16 Apr 2024 17:47:03 +0200
Subject: [PATCH] [Kernel] Add warnings for forward declarations of enums and
tests
---
src/kernel_internals/typing/cabs2cil.ml | 49 ++++++++++---------
tests/syntax/enum_forward.i | 12 +++++
tests/syntax/enum_redef_ko.i | 9 ++++
tests/syntax/enum_redef_ok.i | 8 +++
tests/syntax/oracle/enum_forward.0.res.oracle | 13 +++++
tests/syntax/oracle/enum_forward.1.res.oracle | 17 +++++++
tests/syntax/oracle/enum_redef_ko.res.oracle | 9 ++++
tests/syntax/oracle/enum_redef_ok.res.oracle | 3 ++
8 files changed, 98 insertions(+), 22 deletions(-)
create mode 100644 tests/syntax/enum_forward.i
create mode 100644 tests/syntax/enum_redef_ko.i
create mode 100644 tests/syntax/enum_redef_ok.i
create mode 100644 tests/syntax/oracle/enum_forward.0.res.oracle
create mode 100644 tests/syntax/oracle/enum_forward.1.res.oracle
create mode 100644 tests/syntax/oracle/enum_redef_ko.res.oracle
create mode 100644 tests/syntax/oracle/enum_redef_ok.res.oracle
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index be7ee677ba..858381def9 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -111,9 +111,9 @@ let stripUnderscore s =
Kernel.error ~current:true "unsupported attribute: %s" s
else begin
if not (Ast_attributes.is_known_attribute res) then
- Kernel.warning
- ~once:true ~current:true ~wkey:Kernel.wkey_unknown_attribute
- "Unknown attribute: %s" s
+ Kernel.warning
+ ~once:true ~current:true ~wkey:Kernel.wkey_unknown_attribute
+ "Unknown attribute: %s" s
end;
res
end
@@ -1386,7 +1386,12 @@ let findCompType ghost kind name tattr =
if kind = "enum" then
let enum, isnew = createEnumInfo name ~norig:name in
if isnew then
+ begin
+ Kernel.warning ~wkey:Kernel.wkey_c11
+ ~source:(fst @@ Current_loc.get ())
+ "forward declaration of enum might be rejected by compilers";
cabsPushGlobal (GEnumTagDecl (enum, Current_loc.get ()));
+ end;
mk_tenum ~tattr enum
else
let iss = if kind = "struct" then true else false in
@@ -1697,23 +1702,23 @@ struct
b.bscoping <- b.bscoping || declares_var || not force_non_scoping;
b
| stmts ->
- if c.unspecified_order then begin
+ if c.unspecified_order then begin
if List.length stmts >= 2 then begin
- let first_stmt =
+ let first_stmt =
(fun (s,_,_,_,_) -> s) (Extlib.last stmts) in
- Kernel.warning ~wkey:Kernel.wkey_cert_exp_10
- ~source:(fst (Stmt.loc first_stmt))
- "Potential unsequenced side-effects"
- end;
- let b =
- Cil.mkBlock
+ Kernel.warning ~wkey:Kernel.wkey_cert_exp_10
+ ~source:(fst (Stmt.loc first_stmt))
+ "Potential unsequenced side-effects"
+ end;
+ let b =
+ Cil.mkBlock
[mkStmt ~ghost ~valid_sid (UnspecifiedSequence (List.rev stmts))]
- in
- b.blocals <- vars;
- b.bstatics <- c.statics;
- b.bscoping <- declares_var || not force_non_scoping;
- b
- end else
+ in
+ b.blocals <- vars;
+ b.bstatics <- c.statics;
+ b.bscoping <- declares_var || not force_non_scoping;
+ b
+ end else
let stmts = List.rev_map (fun (s,_,_,_,_) -> s) stmts in
let b = Cil.mkBlock stmts in
b.blocals <- vars;
@@ -4691,9 +4696,9 @@ and cabsPartitionAttributes
and doType (ghost:bool) (context: type_context)
(nameortype: Ast_attributes.attribute_class) (* This is AttrName if we are doing
- * the type for a name, or AttrType
- * if we are doing this type in a
- * typedef *)
+ * the type for a name, or AttrType
+ * if we are doing this type in a
+ * typedef *)
?(allowZeroSizeArrays=false)
?(allowVarSizeArrays=false)
(bt: typ) (* The base type *)
@@ -6510,7 +6515,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))
@@ -9780,7 +9785,7 @@ and doTypedef ghost ((specs, nl): Cabs.name_group) =
if declared_in_current_scope ~ghost n then
begin
match newTyp'.tnode with (* do NOT unroll type here,
- redefinitions of typedefs are ok *)
+ redefinitions of typedefs are ok *)
| TComp newci ->
(* Composite types with different tags may be compatible, but here
we use the tags to try and detect if the type is being redefined,
diff --git a/tests/syntax/enum_forward.i b/tests/syntax/enum_forward.i
new file mode 100644
index 0000000000..f91f820e67
--- /dev/null
+++ b/tests/syntax/enum_forward.i
@@ -0,0 +1,12 @@
+/* run.config
+ STDOPT: -machdep gcc_x86_64
+ STDOPT: -kernel-warn-key c11
+*/
+
+/* forward declaration of enum is supported by GCC but nonstandard */
+
+enum e X;
+enum e { V };
+
+enum g Y;
+typedef enum g { W } g;
diff --git a/tests/syntax/enum_redef_ko.i b/tests/syntax/enum_redef_ko.i
new file mode 100644
index 0000000000..d7358e0ece
--- /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 0000000000..4c4a93c217
--- /dev/null
+++ b/tests/syntax/enum_redef_ok.i
@@ -0,0 +1,8 @@
+/* run.config
+ STDOPT:
+*/
+
+/* "tentative definition" is allowed */
+
+enum e { U };
+enum e;
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 0000000000..a870e09354
--- /dev/null
+++ b/tests/syntax/oracle/enum_forward.0.res.oracle
@@ -0,0 +1,13 @@
+[kernel] Parsing enum_forward.i (no preprocessing)
+/* Generated by Frama-C */
+enum e;
+enum e {
+ V = 0
+};
+enum g;
+enum g {
+ W = 0
+};
+enum e X;
+enum g Y;
+
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 0000000000..9f601ccd94
--- /dev/null
+++ b/tests/syntax/oracle/enum_forward.1.res.oracle
@@ -0,0 +1,17 @@
+[kernel] Parsing enum_forward.i (no preprocessing)
+[kernel:c11] enum_forward.i:8: Warning:
+ forward declaration of enum might be rejected by compilers
+[kernel:c11] enum_forward.i:11: Warning:
+ forward declaration of enum might be rejected by compilers
+/* Generated by Frama-C */
+enum e;
+enum e {
+ V = 0
+};
+enum g;
+enum g {
+ W = 0
+};
+enum e X;
+enum g Y;
+
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 0000000000..93c3071d30
--- /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 0000000000..f7f26829ef
--- /dev/null
+++ b/tests/syntax/oracle/enum_redef_ok.res.oracle
@@ -0,0 +1,3 @@
+[kernel] Parsing enum_redef_ok.i (no preprocessing)
+/* Generated by Frama-C */
+
--
GitLab