diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 5d1ef9ae8d4e6c443623d90b49e6b767b3c67663..3de84577103cb1b6bd7e3a17211be13da4001d09 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -3040,9 +3040,9 @@ let rec collectInitializer | Some len -> begin match constFoldToInt len with | Some ni when Integer.ge ni Integer.zero -> to_integer ni, false - | _ -> - abort_context - "\"Variable length array in structure\" extension is not supported" + | _ -> (* VLA cannot have initializers, and this should have + been captured beforehand. *) + Kernel.fatal "Trying to initialize a variable-length array" end | _ -> (* unsized array case, length comes from initializers *)