From c78ae5db7d8ee8ed32d0bf4c045f0d6d4376537d Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Thu, 6 Dec 2018 18:54:54 +0100
Subject: [PATCH] [Cabs2cil] reject zero-width named bitfields
---
src/kernel_internals/typing/cabs2cil.ml | 6 ++++-
.../oracle/unnamed_bitfields.0.res.oracle | 1 +
.../oracle/unnamed_bitfields.1.res.oracle | 6 +++++
.../oracle/unnamed_bitfields.res.oracle | 18 ---------------
tests/syntax/unnamed_bitfields.c | 23 +++++++++++++++++++
tests/syntax/unnamed_bitfields.i | 8 -------
tests/value/library.i | 2 +-
7 files changed, 36 insertions(+), 28 deletions(-)
create mode 100644 tests/syntax/oracle/unnamed_bitfields.0.res.oracle
create mode 100644 tests/syntax/oracle/unnamed_bitfields.1.res.oracle
delete mode 100644 tests/syntax/oracle/unnamed_bitfields.res.oracle
create mode 100644 tests/syntax/unnamed_bitfields.c
delete mode 100644 tests/syntax/unnamed_bitfields.i
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index ccbe1f20c77..9e04c0ee08b 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -5559,8 +5559,12 @@ and makeCompType ghost (isstruct: bool)
anonCompFieldName ^ (string_of_int !anonCompFieldNameId)
end
| _ -> n
- end else
+ end else begin
+ if fbitfield = Some 0 then
+ Kernel.error ~source:(fst cloc)
+ "named bitfield (%s) with zero width" n;
n
+ end
in
let rec is_circular t =
match Cil.unrollType t with
diff --git a/tests/syntax/oracle/unnamed_bitfields.0.res.oracle b/tests/syntax/oracle/unnamed_bitfields.0.res.oracle
new file mode 100644
index 00000000000..6df296791c5
--- /dev/null
+++ b/tests/syntax/oracle/unnamed_bitfields.0.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing unnamed_bitfields.c (with preprocessing)
diff --git a/tests/syntax/oracle/unnamed_bitfields.1.res.oracle b/tests/syntax/oracle/unnamed_bitfields.1.res.oracle
new file mode 100644
index 00000000000..6a2d6755f07
--- /dev/null
+++ b/tests/syntax/oracle/unnamed_bitfields.1.res.oracle
@@ -0,0 +1,6 @@
+[kernel] Parsing unnamed_bitfields.c (with preprocessing)
+[kernel] unnamed_bitfields.c:15: User Error:
+ named bitfield (zero_with_name) with zero width
+[kernel] User Error: stopping on file "unnamed_bitfields.c" that has errors. Add
+ '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/unnamed_bitfields.res.oracle b/tests/syntax/oracle/unnamed_bitfields.res.oracle
deleted file mode 100644
index 89cfeea2854..00000000000
--- a/tests/syntax/oracle/unnamed_bitfields.res.oracle
+++ /dev/null
@@ -1,18 +0,0 @@
-[kernel] Parsing unnamed_bitfields.i (no preprocessing)
-/* Generated by Frama-C */
-struct foo {
- unsigned int bar : 16 ;
- unsigned int : 0 ;
- unsigned int bla : 11 ;
- unsigned int : 1 ;
- unsigned int bli : 4 ;
- unsigned int : 0 ;
-};
-unsigned int f(struct foo s)
-{
- unsigned int __retres;
- __retres = (unsigned int)s.bla;
- return __retres;
-}
-
-
diff --git a/tests/syntax/unnamed_bitfields.c b/tests/syntax/unnamed_bitfields.c
new file mode 100644
index 00000000000..6f999ad0a8a
--- /dev/null
+++ b/tests/syntax/unnamed_bitfields.c
@@ -0,0 +1,23 @@
+/* run.config
+OPT:
+EXIT:1
+OPT: -cpp-extra-args="-DINVALID_ZERO_BF"
+ */
+
+struct foo
+{
+ unsigned bar : 16, : 0;
+ unsigned bla : 11, : 1;
+ unsigned bli : 4, : 0;
+};
+
+#ifdef INVALID_ZERO_BF
+struct invalid_foo
+{
+ unsigned first : 1;
+ unsigned zero_with_name: 0;
+ unsigned last : 2;
+};
+#endif
+
+unsigned f(struct foo s) { return s.bla; }
diff --git a/tests/syntax/unnamed_bitfields.i b/tests/syntax/unnamed_bitfields.i
deleted file mode 100644
index 14e793c74ab..00000000000
--- a/tests/syntax/unnamed_bitfields.i
+++ /dev/null
@@ -1,8 +0,0 @@
-struct foo
-{
- unsigned bar : 16, : 0;
- unsigned bla : 11, : 1;
- unsigned bli : 4, : 0;
-};
-
-unsigned f(struct foo s) { return s.bla; }
diff --git a/tests/value/library.i b/tests/value/library.i
index 797623ff33b..8a05e158746 100644
--- a/tests/value/library.i
+++ b/tests/value/library.i
@@ -60,7 +60,7 @@ void (*ff)();
struct {
short bf1: 5;
- short bf : 0; // 0-sized bitfield: do not attemp to initialize it
+ short : 0; // 0-sized bitfield: do not attemp to initialize it
unsigned int control: 14, : 0;
} s_bitfield;
--
GitLab