aboutsummaryrefslogtreecommitdiffstats
path: root/extraction
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-04-19 21:14:21 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-04-19 21:14:21 +0200
commiteead578fde08a1555086ed75714bca3ca1f9b1dc (patch)
tree74bb1d0009494bf406d5b677c2c30bed5ba2e2e8 /extraction
parenta95735290d61f50a388895ef86627becd67c4553 (diff)
downloadcompcert-kvx-eead578fde08a1555086ed75714bca3ca1f9b1dc.tar.gz
compcert-kvx-eead578fde08a1555086ed75714bca3ca1f9b1dc.zip
add options for controlling madd and notrap selection
Diffstat (limited to 'extraction')
-rw-r--r--extraction/extraction.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 18637336..b6aa3409 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -142,6 +142,8 @@ Extract Constant Compopts.optim_xsaddr =>
"fun _ -> !Clflags.option_fxsaddr".
Extract Constant Compopts.optim_addx =>
"fun _ -> !Clflags.option_faddx".
+Extract Constant Compopts.optim_madd =>
+ "fun _ -> !Clflags.option_fmadd".
Extract Constant Compopts.optim_coalesce_mem =>
"fun _ -> !Clflags.option_fcoalesce_mem".
Extract Constant Compopts.optim_forward_moves =>