aboutsummaryrefslogtreecommitdiffstats
path: root/extraction
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-05-02 09:32:49 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-05-02 09:32:49 +0200
commit9f256a4ad30c93749e6c1192a84f996feac3b023 (patch)
tree81b381e5651e34474a133f012927442f64d51c56 /extraction
parent053cfa54205575ceb984f5922f51f4fce5980604 (diff)
downloadcompcert-kvx-9f256a4ad30c93749e6c1192a84f996feac3b023.tar.gz
compcert-kvx-9f256a4ad30c93749e6c1192a84f996feac3b023.zip
command line options (still incomplete)
Diffstat (limited to 'extraction')
-rw-r--r--extraction/extraction.v6
1 files changed, 6 insertions, 0 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v
index f58991aa..0f336916 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -117,6 +117,12 @@ Extract Constant Compopts.thumb =>
"fun _ -> !Clflags.option_mthumb".
Extract Constant Compopts.debug =>
"fun _ -> !Clflags.option_g".
+Extract Constant Compopts.optim_fglobaladdrtmp =>
+ "fun _ -> !Clflags.option_fglobaladdrtmp".
+Extract Constant Compopts.optim_fglobaladdroffset =>
+ "fun _ -> !Clflags.option_fglobaladdroffset".
+Extract Constant Compopts.optim_fxsaddr =>
+ "fun _ -> !Clflags.option_fxsaddr".
(* Compiler *)
Extract Constant Compiler.print_Clight => "PrintClight.print_if".