From 7ca7e64ab06d0d4deb6b3b48593f4955cf5c3c5f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 6 Mar 2018 09:59:23 +0100 Subject: 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. --- cparser/Cutil.ml | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'cparser/Cutil.ml') diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 71c253f8..30037049 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -707,6 +707,11 @@ let is_integer_type env t = | TEnum(_, _) -> true | _ -> false +let is_float_type env t = + match unroll env t with + | TFloat (_, _) -> true + | _ -> false + let is_arith_type env t = match unroll env t with | TInt(_, _) -> true @@ -1207,3 +1212,8 @@ let rec subst_stmt phi s = List.map subst_asm_operand inputs, clob) } + +let is_volatile_variable env exp = + match exp.edesc with + | EVar x -> List.mem AVolatile (attributes_of_type env exp.etyp) + | _ -> false -- cgit