diff options
Diffstat (limited to 'exportclight')
| -rw-r--r-- | exportclight/Clightgen.ml | 85 |
1 files changed, 15 insertions, 70 deletions
diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml index f927e5ab..2878cb17 100644 --- a/exportclight/Clightgen.ml +++ b/exportclight/Clightgen.ml @@ -16,12 +16,11 @@ open Printf open Commandline open Clflags +open CommonOptions open Driveraux open Frontend -(* Location of the compatibility library *) - -let stdlib_path = ref Configuration.stdlib_path +let tool_name = "Clight generator" (* clightgen-specific options *) @@ -86,14 +85,8 @@ let process_i_file sourcename = let ofile = output_filename sourcename ".i" in compile_c_file sourcename sourcename ofile -let version_string = - if Version.buildnr <> "" && Version.tag <> "" then - sprintf "The CompCert Clight generator, %s, Build: %s, Tag: %s\n" Version.version Version.buildnr Version.tag - else - "The CompCert Clight generator, version "^ Version.version ^ "\n" - let usage_string = - version_string ^ + version_string tool_name^ {|Usage: clightgen [options] <source files> Recognized source files: .c C source file @@ -104,44 +97,18 @@ Processing options: -o <file> Generate output in <file> |} ^ prepro_help ^ -{|Language support options (use -fno-<opt> to turn off -f<opt>) : - -fbitfields Emulate bit fields in structs [off] - -flongdouble Treat 'long double' as 'double' [off] - -fstruct-passing Support passing structs and unions by value as function - results or function arguments [off] - -fstruct-return Like -fstruct-passing (deprecated) - -fvararg-calls Emulate calls to variable-argument functions [on] - -funprototyped Support calls to old-style functions without prototypes [on] - -fpacked-structs Emulate packed structs [off] - -finline-asm Support inline 'asm' statements [off] - -fall Activate all language support options above - -fnone Turn off all language support options above -Tracing options: +language_support_help ^ +{|Tracing options: -dparse Save C file after parsing and elaboration in <file>.parsed.c -dc Save generated Compcert C in <file>.compcert.c -dclight Save generated Clight in <file>.light.c -General options: - -stdlib <dir> Set the path of the Compcert run-time library - -v Print external commands before invoking them - -version Print the version string and exit - -target <value> Generate code for the given target - -conf <file> Read configuration from file - @<file> Read command line options from <file> |} ^ + general_help ^ Cerrors.warning_help let print_usage_and_exit () = printf "%s" usage_string; exit 0 -let print_version_and_exit () = - printf "%s" version_string; exit 0 - -let language_support_options = [ - option_fbitfields; option_flongdouble; - option_fstruct_passing; option_fvararg_calls; option_funprototyped; - option_fpacked_structs; option_finline_asm -] - let set_all opts () = List.iter (fun r -> r := true) opts let unset_all opts () = List.iter (fun r -> r := false) opts @@ -158,52 +125,30 @@ let perform_actions () = 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 [ (* Getting help *) Exact "-help", Unit print_usage_and_exit; - Exact "--help", Unit print_usage_and_exit; -(* Getting version info *) - Exact "-version", Unit print_version_and_exit; - Exact "--version", Unit print_version_and_exit; + Exact "--help", Unit print_usage_and_exit;] + (* Getting version info *) + @ version_options tool_name @ (* Processing options *) - Exact "-E", Set option_E; + [ Exact "-E", Set option_E; Exact "-normalize", Set option_normalize; Exact "-o", String(fun s -> option_o := Some s); Prefix "-o", Self (fun s -> let s = String.sub s 2 ((String.length s) - 2) in option_o := Some s);] (* Preprocessing options *) @ prepro_actions @ -(* Language support options -- more below *) - [Exact "-fall", Unit (set_all language_support_options); - Exact "-fnone", Unit (unset_all language_support_options); (* Tracing options *) - Exact "-dparse", Set option_dparse; + [ Exact "-dparse", Set option_dparse; Exact "-dc", Set option_dcmedium; - Exact "-dclight", Set option_dclight; -(* General options *) - Exact "-v", Set option_v; - Exact "-stdlib", String(fun s -> stdlib_path := s); - Exact "-stdlib", String(fun s -> stdlib_path := s); - Exact "-conf", Ignore; (* Ignore option since it is already handled *) - Exact "-target", Ignore; (* Ignore option since it is already handled *) - ] + Exact "-dclight", Set option_dclight;] + @ general_options (* Diagnostic options *) @ Cerrors.warning_options -(* -f options: come in -f and -fno- variants *) -(* Language support options *) - @ f_opt "longdouble" option_flongdouble - @ f_opt "struct-return" option_fstruct_passing - @ f_opt "struct-passing" option_fstruct_passing - @ f_opt "bitfields" option_fbitfields - @ f_opt "vararg-calls" option_fvararg_calls - @ f_opt "unprototyped" option_funprototyped - @ f_opt "packed-structs" option_fpacked_structs - @ f_opt "inline-asm" option_finline_asm - @ [ + @ language_support_options @ (* Catch options that are not handled *) - Prefix "-", Self (fun s -> + [Prefix "-", Self (fun s -> eprintf "Unknown option `%s'\n" s; exit 2); (* File arguments *) Suffix ".c", Self (fun s -> |