Check if array length is too large in cabs2cil

src/kernel_internals/typing/cabs2cil.ml

@@ -4794,9 +4794,28 @@ and doType (ghost:bool) isFuncArg
           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."
+             begin
+               if Integer.lt i Integer.zero then
+                 Kernel.error ~once:true ~current:true
+                   "Array length is negative."
+               else
+                 try
+                   (* Check if array length is > SIZE_MAX / sizeof(bt) *)
+                   let elem_size = Integer.of_int @@ bytesSizeOf bt in
+                   let size_t = bitsSizeOfInt theMachine.kindOfSizeOf in
+                   let size_max = Cil.max_unsigned_number size_t in
+                   let limit = Integer.c_div size_max elem_size in
+                   if Integer.gt i limit then
+                     Kernel.error ~once:true ~current:true
+                       "Array length is too large.";
+                 with
+                 | SizeOfError (msg,_) ->
+                   Kernel.abort ~current:true "%s" msg
+                 | Invalid_argument msg ->
+                   Kernel.fatal ~current:true "%s" msg
+                 | Division_by_zero ->
+                   Kernel.fatal ~current:true "Array element size cannot be zero"
+             end
            | _  when not allowVarSizeArrays ->
              if isConstant cst then
                (* e.g., there may be a float constant involved.