From 25b9b003178002360d666919f2e49e7f5f4a36e2 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 4 Feb 2012 19:14:14 +0000 Subject: Merge of the "volatile" branch: - native treatment of volatile accesses in CompCert C's semantics - translation of volatile accesses to built-ins in SimplExpr - native treatment of struct assignment and passing struct parameter by value - only passing struct result by value remains emulated - in cparser, remove emulations that are no longer used - added C99's type _Bool and used it to express || and && more efficiently. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1814 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- driver/Driver.ml | 17 +++++------------ 1 file changed, 5 insertions(+), 12 deletions(-) (limited to 'driver/Driver.ml') diff --git a/driver/Driver.ml b/driver/Driver.ml index cee62501..9813939b 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -69,11 +69,9 @@ let parse_c_file sourcename ifile = (* Simplification options *) let simplifs = "b" (* blocks: mandatory *) - ^ (if !option_fstruct_passing then "s" else "") - ^ (if !option_fstruct_assign then "S" else "") + ^ (if !option_fstruct_return 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 = @@ -333,10 +331,8 @@ Language support options (use -fno- to turn off -f) : -fbitfields Emulate bit fields in structs [off] -flonglong Partial emulation of 'long long' types [on] -flongdouble Treat 'long double' as 'double' [off] - -fstruct-passing Emulate passing structs and unions by value [off] - -fstruct-assign Emulate assignment between structs or unions [off] + -fstruct-return Emulate returning structs and unions by value [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 @@ -374,9 +370,8 @@ Interpreter mode: " let language_support_options = [ - option_fbitfields; option_flonglong; option_flongdouble; option_fstruct_passing; - option_fstruct_assign; option_fvararg_calls; option_fpacked_structs; - option_fvolatile_rmw + option_fbitfields; option_flonglong; option_flongdouble; + option_fstruct_return; option_fvararg_calls; option_fpacked_structs ] let cmdline_actions = @@ -434,14 +429,12 @@ let cmdline_actions = ] @ f_opt "longlong" option_flonglong @ f_opt "longdouble" option_flongdouble - @ f_opt "struct-passing" option_fstruct_passing - @ f_opt "struct-assign" option_fstruct_assign + @ f_opt "struct-return" option_fstruct_return @ f_opt "bitfields" option_fbitfields @ f_opt "vararg-calls" option_fvararg_calls @ 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 }; -- cgit