diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-03-08 16:02:52 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-03-08 16:02:52 +0100 |
| commit | 1c4e0ece041f87cc0c328c94270f2b23facc8b77 (patch) | |
| tree | 64a4d26d1f267edb1f3dc9284e2468c32335f466 /backend/AisAnnot.mli | |
| parent | bbf922a184764a8f79b9e45dd302879568504703 (diff) | |
| download | compcert-kvx-1c4e0ece041f87cc0c328c94270f2b23facc8b77.tar.gz compcert-kvx-1c4e0ece041f87cc0c328c94270f2b23facc8b77.zip | |
Print symbols as symbols.
This allows us to replacing them by their address in valex and
additionally checking them.
Bug 22438
Diffstat (limited to 'backend/AisAnnot.mli')
| -rw-r--r-- | backend/AisAnnot.mli | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/backend/AisAnnot.mli b/backend/AisAnnot.mli index 59676b26..6bed2eaa 100644 --- a/backend/AisAnnot.mli +++ b/backend/AisAnnot.mli @@ -33,3 +33,12 @@ val validate_ais_annot: Env.t -> string * int -> string -> C.exp list -> unit that no volatile variables or float expressions are used as well as that no illegal format specifier is used in the [txt] *) + +val json_ais_annot: ('a -> string) -> string -> string -> 'a AST.builtin_arg list -> t list +(** [json_ais_annot lbl preg spreg txt args] prints the ais annotation [txt] were the format + specifiers are replace according to their type: + -e: general expressions + -l: l-value expressions + -here: the address of the ais annotation [lbl] + for json export. +*) |