diff options
Diffstat (limited to 'cparser')
| -rw-r--r-- | cparser/Cutil.ml | 11 | ||||
| -rw-r--r-- | cparser/Cutil.mli | 2 | ||||
| -rw-r--r-- | cparser/Elab.ml | 1 |
3 files changed, 14 insertions, 0 deletions
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 124560e5..586b4a92 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -642,6 +642,17 @@ let int_representable v nbits sgn = else 0L <= v && v < Int64.shift_left 1L nbits +let valid_array_size env ty v = + match sizeof env ty with + | None -> true (* Incomplete type should be caught later *) + | Some sz -> + let sz = Int64.of_int sz in + let ptr_bits = !Machine.config.sizeof_ptr * 8 - 1 in + if sz = 0L || v <= (Int64.div Int64.max_int sz) then + int_representable (Int64.mul sz v) ptr_bits true + else + false + (* Type of a function definition *) let fundef_typ fd = diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index 715cc123..79975dcf 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -237,6 +237,8 @@ val field_of_dot_access: Env.t -> typ -> string -> field (* Return the field info for a [x.field] access *) val field_of_arrow_access: Env.t -> typ -> string -> field (* Return the field info for a [x->field] access *) +val valid_array_size: Env.t -> typ -> int64 -> bool + (* Test whether the array size fits in half of the address space *) (* Constructors *) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 07351c46..8b38f4c7 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -658,6 +658,7 @@ and elab_type_declarator keep_ty loc env ty kr_ok = function if n < 0L then error loc "size of array is negative"; if n = 0L then warning loc Zero_length_array "zero size arrays are an extension"; + if not (Cutil.valid_array_size env ty n) then error loc "size of array is too large"; Some n | None -> error loc "size of array is not a compile-time constant"; |