aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Configuration.mli
diff options
context:
space:
mode:
authorBernhard Schommer <bschommer@users.noreply.github.com>2017-10-19 13:08:13 +0200
committerGitHub <noreply@github.com>2017-10-19 13:08:13 +0200
commit6a010b47b216c5a6b6e85abcfbba5339bab15dd6 (patch)
tree4c7f8bacd081f023cfd3220b0aac0e186567d051 /driver/Configuration.mli
parenta0f238a3d270edd7042d9852d43e3ec5b9602af2 (diff)
downloadcompcert-kvx-6a010b47b216c5a6b6e85abcfbba5339bab15dd6.tar.gz
compcert-kvx-6a010b47b216c5a6b6e85abcfbba5339bab15dd6.zip
New support for inserting ais-annotations.
The ais annotations can be inserted via the new ais variants of the builtin annotation. They mainly differe in that they have an address format specifier '%addr' which will be replaced by the adress in the binary. The implementation simply prints a label for the builtin call alongside a the text of the annotation as comment and inserts the annotation together as acii string in a separate section 'ais_annotations' and replaces the usages of the address format specifiers by the address of the label of the builtin call.
Diffstat (limited to 'driver/Configuration.mli')
-rw-r--r--driver/Configuration.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/driver/Configuration.mli b/driver/Configuration.mli
index f0bb8f83..b918c169 100644
--- a/driver/Configuration.mli
+++ b/driver/Configuration.mli
@@ -77,3 +77,6 @@ val response_file_style: response_file_style
val gnu_toolchain: bool
(** Does the targeted system use the gnu toolchain *)
+
+val elf_target: bool
+ (** Is the target binary format ELF? *)