From bc0827dfbad298a26c751e07b877b93d82951d20 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@cea.fr>
Date: Thu, 9 Jan 2025 17:19:27 +0100
Subject: [PATCH] [typing] do not accept enum <-> int conversion when
redefining typedefs
---
src/kernel_internals/typing/cabs2cil.ml | 10 ++++++++++
tests/misc/oracle/audit-out.json | 3 ++-
tests/syntax/enum_typedef_redef.i | 8 ++++++++
.../oracle/enum_typedef_redef.res.oracle | 18 ++++++++++++++++++
4 files changed, 38 insertions(+), 1 deletion(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 4d9b99242b3..93e27f61084 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -9811,10 +9811,20 @@ and doTypedef ghost ((specs, nl): Cabs.name_group) =
error_conflicting_types ()
else
warn_c11_redefinition ()
+ | TInt _ -> error_conflicting_types ()
| t ->
Kernel.fatal
~current:true "typeinfo.ttype (%a) should be an Enum"
Cil_datatype.Typ.pretty t)
+ | TInt _ ->
+ (match typeinfo.ttype with
+ | TInt _ -> warn_c11_redefinition ()
+ | TEnum _ -> error_conflicting_types ()
+ | t ->
+ 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/misc/oracle/audit-out.json b/tests/misc/oracle/audit-out.json
index 5a6d4556056..0550e1826f7 100644
--- a/tests/misc/oracle/audit-out.json
+++ b/tests/misc/oracle/audit-out.json
@@ -73,7 +73,8 @@
],
"disabled": [
"CERT:EXP:10", "acsl-float-compare", "c11", "file:not-found",
- "ghost:already-ghost", "parser:decimal-float", "transient-block"
+ "ghost:already-ghost", "parser:decimal-float", "transient-block",
+ "typing:forward-enum"
]
}
},
diff --git a/tests/syntax/enum_typedef_redef.i b/tests/syntax/enum_typedef_redef.i
index 0a1c96c7ae1..2858e9f2778 100644
--- a/tests/syntax/enum_typedef_redef.i
+++ b/tests/syntax/enum_typedef_redef.i
@@ -9,3 +9,11 @@
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_typedef_redef.res.oracle b/tests/syntax/oracle/enum_typedef_redef.res.oracle
index e69de29bb2d..75c247e34e1 100644
--- a/tests/syntax/oracle/enum_typedef_redef.res.oracle
+++ 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.
--
GitLab