From 16c57875c0b56ffb1cbdc962fb522099994ff6d9 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 11 Jan 2022 11:59:25 +0100
Subject: [PATCH] [cabs2cil] abort in some bitfield errors to avoid spurious
messages
---
src/kernel_internals/typing/cabs2cil.ml | 14 ++++-----
.../struct_with_invalid_field.0.res.oracle | 3 ++
.../struct_with_invalid_field.1.res.oracle | 6 ++++
.../struct_with_invalid_field.2.res.oracle | 6 ++++
.../struct_with_invalid_field.3.res.oracle | 6 ++++
.../struct_with_invalid_field.4.res.oracle | 6 ++++
.../struct_with_invalid_field.res.oracle | 9 ------
.../oracle/very_large_integers.0.res.oracle | 7 +----
tests/syntax/struct_with_invalid_field.c | 30 +++++++++++++++++++
tests/syntax/struct_with_invalid_field.i | 17 -----------
10 files changed, 63 insertions(+), 41 deletions(-)
create mode 100644 tests/syntax/oracle/struct_with_invalid_field.0.res.oracle
create mode 100644 tests/syntax/oracle/struct_with_invalid_field.1.res.oracle
create mode 100644 tests/syntax/oracle/struct_with_invalid_field.2.res.oracle
create mode 100644 tests/syntax/oracle/struct_with_invalid_field.3.res.oracle
create mode 100644 tests/syntax/oracle/struct_with_invalid_field.4.res.oracle
delete mode 100644 tests/syntax/oracle/struct_with_invalid_field.res.oracle
create mode 100644 tests/syntax/struct_with_invalid_field.c
delete mode 100644 tests/syntax/struct_with_invalid_field.i
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 9e04c0ee08b..63b72bb5aa3 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -5507,28 +5507,24 @@ and makeCompType ghost (isstruct: bool)
| TInt (_, _) -> ()
| TEnum _ -> ()
| _ ->
- Kernel.error ~once:true ~source
+ Kernel.abort ~once:true ~current:true
"Base type for bitfield is not an integer type");
match isIntegerConstant ghost w with
| None ->
- Kernel.error ~source
+ Kernel.abort ~current:true
"bitfield width is not a valid integer constant";
- (* error does not immediately stop execution.
- Hence, we return a placeholder here.
- *)
- Some 0, ftype
| Some s as w ->
begin
if s < 0 then
- Kernel.error ~source "negative bitfield width (%d)" s;
+ Kernel.abort ~current:true "negative bitfield width (%d)" s;
try
if s > Cil.bitsSizeOf ftype then
- Kernel.error ~source
+ Kernel.error ~current:true
"bitfield width (%d) exceeds its type (%a, %d bits)"
s Cil_printer.pp_typ ftype (Cil.bitsSizeOf ftype)
with
SizeOfError _ ->
- Kernel.fatal ~source
+ Kernel.fatal ~current:true
"Unable to compute size of %a" Cil_printer.pp_typ ftype
end;
let ftype =
diff --git a/tests/syntax/oracle/struct_with_invalid_field.0.res.oracle b/tests/syntax/oracle/struct_with_invalid_field.0.res.oracle
new file mode 100644
index 00000000000..4babdfba70b
--- /dev/null
+++ b/tests/syntax/oracle/struct_with_invalid_field.0.res.oracle
@@ -0,0 +1,3 @@
+[kernel] Parsing struct_with_invalid_field.c (with preprocessing)
+/* Generated by Frama-C */
+
diff --git a/tests/syntax/oracle/struct_with_invalid_field.1.res.oracle b/tests/syntax/oracle/struct_with_invalid_field.1.res.oracle
new file mode 100644
index 00000000000..08f35f292b1
--- /dev/null
+++ b/tests/syntax/oracle/struct_with_invalid_field.1.res.oracle
@@ -0,0 +1,6 @@
+[kernel] Parsing struct_with_invalid_field.c (with preprocessing)
+[kernel] struct_with_invalid_field.c:13: User Error:
+ field `f' declared as a function
+[kernel] User Error: stopping on file "struct_with_invalid_field.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/struct_with_invalid_field.2.res.oracle b/tests/syntax/oracle/struct_with_invalid_field.2.res.oracle
new file mode 100644
index 00000000000..44f758c2e5d
--- /dev/null
+++ b/tests/syntax/oracle/struct_with_invalid_field.2.res.oracle
@@ -0,0 +1,6 @@
+[kernel] Parsing struct_with_invalid_field.c (with preprocessing)
+[kernel] struct_with_invalid_field.c:18: User Error:
+ negative bitfield width (-1)
+[kernel] User Error: stopping on file "struct_with_invalid_field.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/struct_with_invalid_field.3.res.oracle b/tests/syntax/oracle/struct_with_invalid_field.3.res.oracle
new file mode 100644
index 00000000000..b60db2046f2
--- /dev/null
+++ b/tests/syntax/oracle/struct_with_invalid_field.3.res.oracle
@@ -0,0 +1,6 @@
+[kernel] Parsing struct_with_invalid_field.c (with preprocessing)
+[kernel] struct_with_invalid_field.c:18: User Error:
+ negative bitfield width (-2147483648)
+[kernel] User Error: stopping on file "struct_with_invalid_field.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/struct_with_invalid_field.4.res.oracle b/tests/syntax/oracle/struct_with_invalid_field.4.res.oracle
new file mode 100644
index 00000000000..1e059811ea2
--- /dev/null
+++ b/tests/syntax/oracle/struct_with_invalid_field.4.res.oracle
@@ -0,0 +1,6 @@
+[kernel] Parsing struct_with_invalid_field.c (with preprocessing)
+[kernel] struct_with_invalid_field.c:18: User Error:
+ named bitfield (d) with zero width
+[kernel] User Error: stopping on file "struct_with_invalid_field.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/struct_with_invalid_field.res.oracle b/tests/syntax/oracle/struct_with_invalid_field.res.oracle
deleted file mode 100644
index dd110c6d7c9..00000000000
--- a/tests/syntax/oracle/struct_with_invalid_field.res.oracle
+++ /dev/null
@@ -1,9 +0,0 @@
-[kernel] Parsing struct_with_invalid_field.i (no preprocessing)
-[kernel] struct_with_invalid_field.i:8: User Error:
- field `f' declared as a function
-[kernel] struct_with_invalid_field.i:14: User Error:
- negative bitfield width (-1)
-[kernel] struct_with_invalid_field.i:15: User Error:
- negative bitfield width (-2147483648)
-[kernel] User Error: stopping on file "struct_with_invalid_field.i" that has errors.
-[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.0.res.oracle b/tests/syntax/oracle/very_large_integers.0.res.oracle
index 070b0b0891f..2d2a9cccb8a 100644
--- a/tests/syntax/oracle/very_large_integers.0.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.0.res.oracle
@@ -1,13 +1,8 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
[kernel] very_large_integers.c:25: User Error:
integer constant too large in expression (unsigned long long)999999999999999999 + 9999999999999999999
-[kernel] very_large_integers.c:26: User Error:
+[kernel] very_large_integers.c:25: User Error:
bitfield width is not a valid integer constant
-[kernel] very_large_integers.c:74: Warning:
- ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:74: Warning:
- ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
- (9223372036854775808) )
[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/struct_with_invalid_field.c b/tests/syntax/struct_with_invalid_field.c
new file mode 100644
index 00000000000..527c15e35e0
--- /dev/null
+++ b/tests/syntax/struct_with_invalid_field.c
@@ -0,0 +1,30 @@
+/* run.config*
+ STDOPT:
+ EXIT: 1
+ STDOPT: #"-cpp-extra-args=-DFUNTYPE"
+ STDOPT: #"-cpp-extra-args=-DNEG1"
+ STDOPT: #"-cpp-extra-args=-DNEG2"
+ STDOPT: #"-cpp-extra-args=-DNAMEDZERO"
+*/
+
+#ifdef FUNTYPE
+// invalid field with function type, parsing should fail
+struct {
+ void f(int);
+} s;
+#endif
+
+// negative-width bitfields, parsing should fail
+struct neg_bf
+{
+#ifdef NEG1
+ int a:(-1); // invalid
+#endif
+#ifdef NEG2
+ int b:(-2147483647-1); // invalid
+#endif
+#ifdef NAMEDZERO
+ int d:(-0); // invalid (named zero-width)
+#endif
+ int :(-0); // valid (unnamed zero-width)
+};
diff --git a/tests/syntax/struct_with_invalid_field.i b/tests/syntax/struct_with_invalid_field.i
deleted file mode 100644
index c1c4e15224e..00000000000
--- a/tests/syntax/struct_with_invalid_field.i
+++ /dev/null
@@ -1,17 +0,0 @@
-/* run.config*
- EXIT: 1
- STDOPT:
-*/
-
-// invalid field with function type, parsing should fail
-struct {
- void f(int);
-} s;
-
-// negative-width bitfields, parsing should fail
-struct neg_bf
-{
- int a:(-1); // invalid
- int b:(-2147483647-1); // invalid
- int d:(-0); // valid
-};
--
GitLab