diff options
author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2018-03-06 09:59:23 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-03-06 09:59:23 +0100 |
commit | 7ca7e64ab06d0d4deb6b3b48593f4955cf5c3c5f (patch) | |
tree | 550a1a180c7296a125f6f8e5813460e2c078127b /cparser/Cutil.mli | |
parent | 086c6686ec93cdaf7b6433cffdc4d8403a06f8b6 (diff) | |
download | compcert-kvx-7ca7e64ab06d0d4deb6b3b48593f4955cf5c3c5f.tar.gz compcert-kvx-7ca7e64ab06d0d4deb6b3b48593f4955cf5c3c5f.zip |
Reactivated and improved ais annotations.
The ais annotations are now handled in a separate file shared
between all architectures. Also two different variants of
replacements are supported, %e which expands to ais expressions
and %l which also expands to an ais expression but is guaranted to
be usable as l-value in the ais annotation. Otherwise the new
warning is Wrong_is_parameter is generated.
Also an error message is generated if floating point variables are
used in ais annotations since a3 does not support them at the
moment.
Additionally an error message is generated for plain volatile
variables used, since they will enforce a volatile load and result
in the value being passed to the annotation instead of the address
as other global variables.
Diffstat (limited to 'cparser/Cutil.mli')
-rw-r--r-- | cparser/Cutil.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index 79975dcf..87a69f12 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -141,6 +141,8 @@ val is_void_type : Env.t -> typ -> bool (* Is type [void]? *) val is_integer_type : Env.t -> typ -> bool (* Is type integer? *) +val is_float_type : Env.t -> typ -> bool + (* Is type float *) val is_arith_type : Env.t -> typ -> bool (* Is type integer or float? *) val is_pointer_type : Env.t -> typ -> bool @@ -239,6 +241,8 @@ 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 *) +val is_volatile_variable: Env.t -> exp -> bool + (* Test whether the expression is an access to a volatile variable *) (* Constructors *) |