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 /backend/AisAnnot.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 'backend/AisAnnot.mli')
| -rw-r--r-- | backend/AisAnnot.mli | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/backend/AisAnnot.mli b/backend/AisAnnot.mli new file mode 100644 index 00000000..7219369c --- /dev/null +++ b/backend/AisAnnot.mli @@ -0,0 +1,31 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +type t = + | Label of int (** label argument, used for current location*) + | String of string (** text part of the ais annotation *) + | Symbol of AST.ident (** symbol argument, used in variable and function addresses *) + +val add_ais_annot : int -> ('a -> string) -> string -> string -> 'a AST.builtin_arg list -> unit +(** [add_ais_annot lbl preg spreg txt args] adds the ais annotation [txt] were the format + specifiers are replace according to their type: + -a: area definitions + -e: general expressions + -l: l-value expressions + -p: program location + -here: the address of the ais annotation [lbl] + and [preg] is used to get the names of the registers, as well as [spreg] the name of the + stack pointer and [args] the arguments reference in the replacements +*) + +val get_ais_annots: unit -> (t list) list +(** [get_ais_annots ()] return the list of all ais annotations and reset it *) |