diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-02-21 14:01:51 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-02-21 14:01:51 +0100 |
commit | 1e867c804ed11200c8ed1a55a71f416977249363 (patch) | |
tree | f2acbb3d45d27b403840ef35b38b0159285f2ab6 /cparser/Cutil.ml | |
parent | a83df40c59f8b3c50581304fb6c0d3913acf15c7 (diff) | |
download | compcert-1e867c804ed11200c8ed1a55a71f416977249363.tar.gz compcert-1e867c804ed11200c8ed1a55a71f416977249363.zip |
Added check for large arrays.
The check tests whether the size calculation of an array overflows
or the array covers half of the available address space and reports
an error in this case.
Bug 21034
Diffstat (limited to 'cparser/Cutil.ml')
-rw-r--r-- | cparser/Cutil.ml | 11 |
1 files changed, 11 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 = |