From 2476cc4922afb41ec54b742630a8c4740ca1ddff Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Wed, 5 Feb 2020 17:15:20 +0100
Subject: [PATCH] [kernel] Rework some error messages about illegal length in
array.
---
src/kernel_internals/typing/cabs2cil.ml | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index ffa5db94b5b..46b7e6265fa 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -3360,7 +3360,7 @@ let rec collectInitializer
(Integer.to_int ni), false
| _ ->
Kernel.fatal ~current:true
- "Array length is not a constant expression %a"
+ "Array length %a is not a compile-time constant."
Cil_printer.pp_exp len
end
| _ ->
@@ -3678,7 +3678,7 @@ let integerArrayLength (leno: exp option) : int =
try lenOfArray leno
with LenOfArray ->
Kernel.fatal ~current:true
- "Initializing non-constant-length array with length=%a"
+ "Array length %a is not a compile-time constant."
Cil_printer.pp_exp len
let find_field_offset cond (fidlist: fieldinfo list) : offset =
@@ -5074,7 +5074,7 @@ and doType (ghost:bool) isFuncArg
| Const(CInt64(i, _, _)) ->
if Integer.lt i Integer.zero then
Kernel.error ~once:true ~current:true
- "Length of array is negative"
+ "Array length is negative."
| _ ->
if isConstant cst then
(* e.g., there may be a float constant involved.
@@ -5086,7 +5086,7 @@ and doType (ghost:bool) isFuncArg
Cil_printer.pp_exp cst
else
Kernel.error ~once:true ~current:true
- "Length of array is not a constant: %a"
+ "Array length %a is not a compile-time constant."
Cil_printer.pp_exp cst)
end;
if Cil.isZero len' && not allowZeroSizeArrays &&
--
GitLab