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.mli | |
| parent | a83df40c59f8b3c50581304fb6c0d3913acf15c7 (diff) | |
| download | compcert-kvx-1e867c804ed11200c8ed1a55a71f416977249363.tar.gz compcert-kvx-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.mli')
| -rw-r--r-- | cparser/Cutil.mli | 2 |
1 files changed, 2 insertions, 0 deletions
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 *) |