From cafb76e835b5a4d12edb251bff487afb680d870c Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 11 Jan 2022 14:58:27 +0100
Subject: [PATCH] [cabs2cil] improve some error message locations
---
src/kernel_internals/typing/cabs2cil.ml | 11 ++++++-----
.../oracle/struct_with_invalid_field.2.res.oracle | 2 +-
.../oracle/struct_with_invalid_field.3.res.oracle | 2 +-
.../oracle/struct_with_invalid_field.4.res.oracle | 2 +-
tests/syntax/oracle/unnamed_bitfields.1.res.oracle | 2 +-
tests/syntax/oracle/very_large_integers.0.res.oracle | 2 +-
tests/value/library.i | 2 +-
7 files changed, 12 insertions(+), 11 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 63b72bb5aa3..f6aebe306d4 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -5503,28 +5503,29 @@ and makeCompType ghost (isstruct: bool)
match widtho with
| None -> None, ftype
| Some w -> begin
+ let source = fst w.expr_loc in
(match unrollType ftype with
| TInt (_, _) -> ()
| TEnum _ -> ()
| _ ->
- Kernel.abort ~once:true ~current:true
+ Kernel.abort ~once:true ~source
"Base type for bitfield is not an integer type");
match isIntegerConstant ghost w with
| None ->
- Kernel.abort ~current:true
+ Kernel.abort ~source
"bitfield width is not a valid integer constant";
| Some s as w ->
begin
if s < 0 then
- Kernel.abort ~current:true "negative bitfield width (%d)" s;
+ Kernel.abort ~source "negative bitfield width (%d)" s;
try
if s > Cil.bitsSizeOf ftype then
- Kernel.error ~current:true
+ Kernel.error ~source
"bitfield width (%d) exceeds its type (%a, %d bits)"
s Cil_printer.pp_typ ftype (Cil.bitsSizeOf ftype)
with
SizeOfError _ ->
- Kernel.fatal ~current:true
+ Kernel.fatal ~source
"Unable to compute size of %a" Cil_printer.pp_typ ftype
end;
let ftype =
diff --git a/tests/syntax/oracle/struct_with_invalid_field.2.res.oracle b/tests/syntax/oracle/struct_with_invalid_field.2.res.oracle
index 44f758c2e5d..74ab8ae4929 100644
--- a/tests/syntax/oracle/struct_with_invalid_field.2.res.oracle
+++ b/tests/syntax/oracle/struct_with_invalid_field.2.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing struct_with_invalid_field.c (with preprocessing)
-[kernel] struct_with_invalid_field.c:18: User Error:
+[kernel] struct_with_invalid_field.c:21: 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.
diff --git a/tests/syntax/oracle/struct_with_invalid_field.3.res.oracle b/tests/syntax/oracle/struct_with_invalid_field.3.res.oracle
index b60db2046f2..9f48a481b14 100644
--- a/tests/syntax/oracle/struct_with_invalid_field.3.res.oracle
+++ b/tests/syntax/oracle/struct_with_invalid_field.3.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing struct_with_invalid_field.c (with preprocessing)
-[kernel] struct_with_invalid_field.c:18: User Error:
+[kernel] struct_with_invalid_field.c:24: 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.
diff --git a/tests/syntax/oracle/struct_with_invalid_field.4.res.oracle b/tests/syntax/oracle/struct_with_invalid_field.4.res.oracle
index 1e059811ea2..b1712e7f4e0 100644
--- a/tests/syntax/oracle/struct_with_invalid_field.4.res.oracle
+++ b/tests/syntax/oracle/struct_with_invalid_field.4.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing struct_with_invalid_field.c (with preprocessing)
-[kernel] struct_with_invalid_field.c:18: User Error:
+[kernel] struct_with_invalid_field.c:27: 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.
diff --git a/tests/syntax/oracle/unnamed_bitfields.1.res.oracle b/tests/syntax/oracle/unnamed_bitfields.1.res.oracle
index 6a2d6755f07..7e979a78da8 100644
--- a/tests/syntax/oracle/unnamed_bitfields.1.res.oracle
+++ b/tests/syntax/oracle/unnamed_bitfields.1.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing unnamed_bitfields.c (with preprocessing)
-[kernel] unnamed_bitfields.c:15: User Error:
+[kernel] unnamed_bitfields.c:18: 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.
diff --git a/tests/syntax/oracle/very_large_integers.0.res.oracle b/tests/syntax/oracle/very_large_integers.0.res.oracle
index 2d2a9cccb8a..1236cc7d725 100644
--- a/tests/syntax/oracle/very_large_integers.0.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.0.res.oracle
@@ -1,7 +1,7 @@
[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:25: User Error:
+[kernel] very_large_integers.c:26: User Error:
bitfield width is not a valid integer constant
[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/value/library.i b/tests/value/library.i
index 8a05e158746..a7de6191a45 100644
--- a/tests/value/library.i
+++ b/tests/value/library.i
@@ -60,7 +60,7 @@ void (*ff)();
struct {
short bf1: 5;
- short : 0; // 0-sized bitfield: do not attemp to initialize it
+ short : 0; // 0-sized bitfield: do not attempt to initialize it
unsigned int control: 14, : 0;
} s_bitfield;
--
GitLab