Merge branch 'feature/michele/abort-on-illegal-array-length' into 'master'

Rework error messages on illegal array length

See merge request frama-c/frama-c!2524

src/kernel_internals/typing/cabs2cil.ml

@@ -3360,7 +3360,8 @@ 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: \
+                 no explicit initializer allowed."
                 Cil_printer.pp_exp len
           end
         | _ ->
@@ -3678,7 +3679,8 @@ 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: \
+         no explicit initializer allowed."
         Cil_printer.pp_exp len
 
 let find_field_offset cond (fidlist: fieldinfo list) : offset =
@@ -5067,28 +5069,27 @@ and doType (ghost:bool) isFuncArg
             Kernel.error ~once:true ~current:true
               "Array length %a does not have an integral type."
               Cil_printer.pp_exp len';
-          if not allowVarSizeArrays then begin
-            (* Assert that len' is a constant *)
-            let cst = constFold true len' in
-            (match cst.enode with
-             | Const(CInt64(i, _, _)) ->
-               if Integer.lt i Integer.zero then
-                 Kernel.error ~once:true ~current:true
-                   "Length of array is negative"
-             | _ ->
-               if isConstant cst then
-                 (* e.g., there may be a float constant involved.
-                  * We'll leave it to the user to ensure the length is
-                  * non-negative, etc.*)
-                 Kernel.warning ~once:true ~current:true
-                   "Unable to do constant-folding on array length %a. \
-                    Some CIL operations on this array may fail."
-                   Cil_printer.pp_exp cst
-               else
-                 Kernel.error ~once:true ~current:true
-                   "Length of array is not a constant: %a"
-                   Cil_printer.pp_exp cst)
-          end;
+          (* Check that len' is admissible *)
+          let cst = constFold true len' in
+          (match cst.enode with
+           | Const(CInt64(i, _, _)) ->
+             if Integer.lt i Integer.zero then
+               Kernel.error ~once:true ~current:true
+                 "Array length is negative."
+           | _  when not allowVarSizeArrays ->
+             if isConstant cst then
+               (* e.g., there may be a float constant involved.
+                * We'll leave it to the user to ensure the length is
+                * non-negative, etc.*)
+               Kernel.warning ~once:true ~current:true
+                 "Unable to do constant-folding on array length %a. \
+                  Some CIL operations on this array may fail."
+                 Cil_printer.pp_exp cst
+             else
+               Kernel.error ~once:true ~current:true
+                 "Array length %a is not a compile-time constant."
+                 Cil_printer.pp_exp cst
+           | _ -> ());
           if Cil.isZero len' && not allowZeroSizeArrays &&
              not (Cil.gccMode () || Cil.msvcMode ())
           then

tests/syntax/array_size.i

+int f(int t[-1]) { return t[0]; } // should raise an error

tests/syntax/oracle/array_size.res.oracle

+[kernel] Parsing tests/syntax/array_size.i (no preprocessing)
+[kernel] tests/syntax/array_size.i:1: User Error: Array length is negative.
+[kernel] User Error: stopping on file "tests/syntax/array_size.i" that has errors.
+[kernel] Frama-C aborted: invalid user input.