aboutsummaryrefslogtreecommitdiffstats
path: root/driver
diff options
context:
space:
mode:
Diffstat (limited to 'driver')
-rw-r--r--driver/Clflags.ml1
-rw-r--r--driver/Driver.ml5
2 files changed, 6 insertions, 0 deletions
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 08e4a536..81d4af3a 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -17,6 +17,7 @@ let linker_options = ref ([]: string list)
let exe_name = ref "a.out"
let option_flonglong = ref false
let option_fmadd = ref false
+let option_fsda = ref false
let option_dclight = ref false
let option_dasm = ref false
let option_E = ref false
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 30d4a6cc..77f8b828 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -264,6 +264,7 @@ Preprocessing options:
Compilation options:
-flonglong Treat 'long long' as 'long' and 'long double' as 'double'
-fmadd Use fused multiply-add and multiply-sub instructions
+ -fsda Use small data area
-dclight Save generated Clight in <file>.light.c
-dasm Save generated assembly in <file>.s
Linking options:
@@ -303,6 +304,10 @@ let rec parse_cmdline i =
option_fmadd := true;
parse_cmdline (i + 1)
end else
+ if s = "-fsda" then begin
+ option_fsda := true;
+ parse_cmdline (i + 1)
+ end else
if s = "-dclight" then begin
option_dclight := true;
parse_cmdline (i + 1)