diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 4282f0e9f46d53aee4dc7b2f52b9773606f1a9bc..69701e3eda820732a65a4a49f04dca437c6742b2 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -5476,6 +5476,8 @@ and makeCompType ghost (isstruct: bool) Some 0, ftype | Some s as w -> begin + if s < 0 then + Kernel.error ~current:true "negative bitfield width (%d)" s; try if s > Cil.bitsSizeOf ftype then Kernel.error ~current:true