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.

6 files changed, 24 insertions, 3 deletions

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
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 *)
 
diff --git a/cparser/Diagnostics.ml b/cparser/Diagnostics.ml
index fbdc9297..e3258a38 100644
--- a/cparser/Diagnostics.ml
+++ b/cparser/Diagnostics.ml
@@ -90,6 +90,7 @@ type warning_type =
   | Inline_asm_sdump
   | Unused_variable
   | Unused_parameter
+  | Wrong_ais_parameter
 
 (* List of active warnings *)
 let active_warnings: warning_type list ref = ref [
@@ -110,6 +111,7 @@ let active_warnings: warning_type list ref = ref [
   Return_type;
   Literal_range;
   Inline_asm_sdump;
+  Wrong_ais_parameter;
 ]
 
 (* List of errors treated as warning *)
@@ -139,6 +141,7 @@ let string_of_warning = function
   | Inline_asm_sdump -> "inline-asm-sdump"
   | Unused_variable -> "unused-variable"
   | Unused_parameter -> "unused-parameter"
+  | Wrong_ais_parameter -> "wrong-ais-parameter"
 
 (* Activate the given warning *)
 let activate_warning w () =
@@ -184,7 +187,8 @@ let wall () =
     CompCert_conformance;
     Inline_asm_sdump;
     Unused_variable;
-    Unused_parameter
+    Unused_parameter;
+    Wrong_ais_parameter;
   ]
 
 let wnothing () =
@@ -214,6 +218,7 @@ let werror () =
     CompCert_conformance;
     Inline_asm_sdump;
     Unused_variable;
+    Wrong_ais_parameter;
   ]
 
 (* Generate the warning key for the message *)
@@ -390,6 +395,7 @@ let warning_options =
   error_option Inline_asm_sdump @
   error_option Unused_variable @
   error_option Unused_parameter @
+  error_option Wrong_ais_parameter @
   [Exact ("-Wfatal-errors"), Set error_fatal;
    Exact ("-fdiagnostics-color"), Ignore; (* Either output supports it or no color *)
    Exact ("-fno-diagnostics-color"), Unset color_diagnostics;
diff --git a/cparser/Diagnostics.mli b/cparser/Diagnostics.mli
index 82edd9fa..648d537b 100644
--- a/cparser/Diagnostics.mli
+++ b/cparser/Diagnostics.mli
@@ -47,6 +47,7 @@ type warning_type =
   | Inline_asm_sdump               (** inline assembler used in combination of sdump *)
   | Unused_variable                (** unused local variables *)
   | Unused_parameter               (** unused function parameter *)
+  | Wrong_ais_parameter            (** wrong parameter type for ais replacement *)
 
 val warning  : (string * int) -> warning_type -> ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a
 (** [warning (f,c) w fmt arg1 ... argN] formats the arguments [arg1] to [argN] as warining according to
diff --git a/cparser/Parse.ml b/cparser/Parse.ml
index 8143954b..b2c83698 100644
--- a/cparser/Parse.ml
+++ b/cparser/Parse.ml
@@ -69,7 +69,7 @@ let preprocessed_file transfs name sourcefile =
              | Parser.Parser.Inter.Fail_pr ->
                  (* Theoretically impossible : implies inconsistencies
                     between grammars. *)
-                 Diagnostics.fatal_error Diagnostics.no_loc "Internal error while parsing"
+               Diagnostics.fatal_error Diagnostics.no_loc "Internal error while parsing"
              | Parser.Parser.Inter.Timeout_pr -> assert false
              | Parser.Parser.Inter.Parsed_pr (ast, _ ) -> ast) in
       let p1 = Timing.time "Elaboration" Elab.elab_file ast in
diff --git a/cparser/Rename.ml b/cparser/Rename.ml
index cdb5751e..d63fa47d 100644
--- a/cparser/Rename.ml
+++ b/cparser/Rename.ml
@@ -84,7 +84,7 @@ let ident env id =
     IdentMap.find id env.re_id
   with Not_found ->
     Diagnostics.fatal_error Diagnostics.no_loc "internal error: rename: %s__%d unbound"
-                        id.name id.stamp
+      id.name id.stamp
 
 let rec typ env = function
   | TPtr(ty, a) -> TPtr(typ env ty, a)