aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Driver.ml
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-05-29 11:43:29 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-05-29 11:43:29 +0200
commitd075968e1e516ab80460afce57c9bcc15d206c19 (patch)
treea5da5b20f193058ae85aafadcffea6b3b2b9f9a5 /driver/Driver.ml
parent11cd0ace897752ef7ca33609aa1250ca1597185b (diff)
downloadcompcert-kvx-d075968e1e516ab80460afce57c9bcc15d206c19.tar.gz
compcert-kvx-d075968e1e516ab80460afce57c9bcc15d206c19.zip
added -fdiv-i32 and -fdiv-i64 options
Diffstat (limited to 'driver/Driver.ml')
-rw-r--r--driver/Driver.ml12
1 files changed, 9 insertions, 3 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml
index cfafcaa3..314cf31c 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -265,9 +265,13 @@ let num_input_files = ref 0
let cmdline_actions =
let f_opt name ref =
[Exact("-f" ^ name), Set ref; Exact("-fno-" ^ name), Unset ref] in
- let f_opt_str name ref strref =
+ let f_opt_str name ref strref default =
[Exact("-f" ^ name ^ "="), String
- (fun s -> (strref := (if s == "" then "list" else s)); ref := true)
+ (fun s -> (strref := (if s == "" then default else s)); ref := true)
+ ] in
+ let f_str name strref default =
+ [Exact("-f" ^ name ^ "="), String
+ (fun s -> (strref := (if s == "" then default else s)))
] in
[
(* Getting help *)
@@ -369,13 +373,15 @@ let cmdline_actions =
@ f_opt "cse" option_fcse
@ f_opt "redundancy" option_fredundancy
@ f_opt "postpass" option_fpostpass
- @ f_opt_str "postpass" option_fpostpass option_fpostpass_sched
+ @ f_opt_str "postpass" option_fpostpass option_fpostpass_sched "list"
@ f_opt "inline" option_finline
@ f_opt "inline-functions-called-once" option_finline_functions_called_once
@ f_opt "globaladdrtmp" option_fglobaladdrtmp
@ f_opt "globaladdroffset" option_fglobaladdroffset
@ f_opt "xsaddr" option_fxsaddr
@ f_opt "coalesce-mem" option_coalesce_mem
+ @ f_str "div-i32" option_div_i32 "stsud"
+ @ f_str "div-i64" option_div_i64 "stsud"
(* Code generation options *)
@ f_opt "fpu" option_ffpu
@ f_opt "sse" option_ffpu (* backward compatibility *)