summaryrefslogtreecommitdiff
path: root/driver
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2011-08-18 14:50:19 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2011-08-18 14:50:19 +0000
commit50ee6bdf639ffba989968abb9c24a57126ab35a4 (patch)
tree80e123d295a84372b13739b6905d583fa9bbe700 /driver
parent62a07ee96d51c29bab9668d8c41bf5f8bdf9e23d (diff)
Presimplification SimplVolatile: cleaned up and integrated.
test/*/Makefile: normalized 'bench' target git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1717 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'driver')
-rw-r--r--driver/Clflags.ml1
-rw-r--r--driver/Driver.ml17
2 files changed, 17 insertions, 1 deletions
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 87de59f..fe14ba7 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -21,6 +21,7 @@ let option_fstruct_assign = ref false
let option_fbitfields = ref false
let option_fvararg_calls = ref true
let option_fpacked_structs = ref false
+let option_fvolatile_rmw = ref true
let option_fmadd = ref false
let option_fsse = ref true
let option_dparse = ref false
diff --git a/driver/Driver.ml b/driver/Driver.ml
index d5a659d..1139e7a 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -73,6 +73,7 @@ let parse_c_file sourcename ifile =
^ (if !option_fstruct_assign then "S" else "")
^ (if !option_fbitfields then "f" else "")
^ (if !option_fpacked_structs then "p" else "")
+ ^ (if !option_fvolatile_rmw then "v" else "")
in
(* Parsing and production of a simplified C AST *)
let ast =
@@ -340,7 +341,10 @@ Language support options (use -fno-<opt> to turn off -f<opt>) :
-fstruct-passing Emulate passing structs and unions by value [off]
-fstruct-assign Emulate assignment between structs or unions [off]
-fvararg-calls Emulate calls to variable-argument functions [on]
+ -fvolatile-rmw Emulate ++, -- and op= on volatile l-values [on]
-fpacked-structs Emulate packed structs [off]
+ -fall Activate all language support options above
+ -fnone Turn off all language support options above
Code generation options: (use -fno-<opt> to turn off -f<opt>) :
-fmadd (PowerPC) Use fused multiply-add and multiply-sub instructions [off]
-fsse (IA32) Use SSE2 instructions for some integer operations [on]
@@ -374,6 +378,12 @@ Interpreter mode:
-all Simulate all possible execution orders
"
+let language_support_options = [
+ option_fbitfields; option_flonglong; option_fstruct_passing;
+ option_fstruct_assign; option_fvararg_calls; option_fpacked_structs;
+ option_fvolatile_rmw
+]
+
let cmdline_actions =
let f_opt name ref =
["-f" ^ name ^ "$", Set ref; "-fno-" ^ name ^ "$", Unset ref] in
@@ -421,7 +431,11 @@ let cmdline_actions =
".*\\.[oa]$", Self (fun s ->
linker_options := s :: !linker_options);
"-fsmall-data$", Integer(fun n -> option_small_data := n);
- "-fsmall-const$", Integer(fun n -> option_small_const := n)
+ "-fsmall-const$", Integer(fun n -> option_small_const := n);
+ "-fall$", Self (fun _ ->
+ List.iter (fun r -> r := true) language_support_options);
+ "-fnone$", Self (fun _ ->
+ List.iter (fun r -> r := false) language_support_options);
]
@ f_opt "longlong" option_flonglong
@ f_opt "struct-passing" option_fstruct_passing
@@ -431,6 +445,7 @@ let cmdline_actions =
@ f_opt "madd" option_fmadd
@ f_opt "packed-structs" option_fpacked_structs
@ f_opt "sse" option_fsse
+ @ f_opt "volatile-rmw" option_fvolatile_rmw
let _ =
Gc.set { (Gc.get()) with Gc.minor_heap_size = 524288 };