diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 63b72bb5aa336b8964bebb9f1a20127413b86609..f6aebe306d45681b089a7e5e8c08a75260f7e139 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 44f758c2e5d8d9630c9058f1f041f4b8b2e5fcb4..74ab8ae4929831eabb086c70a64621a0a51abc77 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 b60db2046f2598184d7fc86ee722f5403d872499..9f48a481b14d8c7fa5a5e78205a394a884da326d 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 1e059811ea2a618d20d1d96587c2897c1cd5b1be..b1712e7f4e0211385f08c79380d7d19887ef3f4c 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 6a2d6755f07d2ab66cadfca255217ee9fcb50a8c..7e979a78da83b634c71c301194a1088e2b259f8f 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 2d2a9cccb8aa58b64d43325cda4135e660e12438..1236cc7d7251b2e8c568575ebd87c1f5fe81ecbc 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 8a05e15874684493bbaa0d8ea10a1ef561044460..a7de6191a45e32d95a96bfde962081c2891b47a3 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;