diff options
Diffstat (limited to 'driver')
-rw-r--r-- | driver/Driver.ml | 144 | ||||
-rw-r--r-- | driver/Frontend.ml | 97 |
2 files changed, 131 insertions, 110 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index b8c92d6c..5a7bd929 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -293,6 +293,51 @@ let version_string = else "The CompCert C verified compiler, version "^ Version.version ^ "\n" +let gnu_system = Configuration.system <> "diab" + +let gnu_debugging_help = +" -gdwarf- Generate debug information in DWARF v2 or DWARF v3\n" + +let debugging_help = +"Debugging options:\n\ +\ -g Generate debugging information\n\ +\ -gdepth <n> Control generation of debugging information\n\ +\ (<n>=0: none, <n>=1: only-globals, <n>=2: globals + locals\n\ +\ without locations, <n>=3: full;)\n" +^ (if gnu_system then gnu_debugging_help else "")^ +" -frename-static Rename static functions and declarations\n" + +let target_help = if Configuration.arch = "arm" then +"Target processor options:\n\ +\ -mthumb Use Thumb2 instruction encoding\n\ +\ -marm Use classic ARM instruction encoding\n" +else + "" + +let gnu_linker_help = +" -nostartfiles Do not use the standard system startup files when\n\ +\ linking\n\ +\ -nodefaultlibs Do not use the standard system libraries when\n\ +\ linking\n\ +\ -nostdlib Do not use the standard system startup files or\n\ +\ libraries when linking\n" + +let linker_help = +"Linking options:\n\ +\ -l<lib> Link library <lib>\n\ +\ -L<dir> Add <dir> to search path for libraries\n" ^ + (if gnu_system then gnu_linker_help else "") ^ +" -s Remove all symbol table and relocation information from the\n\ +\ executable\n\ +\ -static Prevent linking with the shared libraries\n\ +\ -T <file> Use <file> as linker command file\n\ +\ -Wl,<opt> Pass option <opt> to the linker\n\ +\ -WUl,<opt> Pass option <opt> to the gcc or dcc used for linking\n\ +\ -Xlinker <opt> Pass <opt> as an option to the linker\n\ +\ -u <symb> Pretend the symbol <symb> is undefined to force linking of\n\ +\ library modules to define it.\n" + + let usage_string = version_string ^ "Usage: ccomp [options] <source files>\n\ @@ -321,15 +366,9 @@ Processing options:\n\ \ -fpacked-structs Emulate packed structs [off]\n\ \ -finline-asm Support inline 'asm' statements [off]\n\ \ -fall Activate all language support options above\n\ -\ -fnone Turn off all language support options above\n\ -Debugging options:\n\ -\ -g Generate debugging information\n\ -\ -gdwarf- (GCC only) Generate debug information in DWARF v2 or DWARF v3\n\ -\ -gdepth <n> Control generation of debugging information\n\ -\ (<n>=0: none, <n>=1: only-globals, <n>=2: globals + locals\n\ -\ without locations, <n>=3: full;)\n\ -\ -frename-static Rename static functions and declarations\n\ -Optimization options: (use -fno-<opt> to turn off -f<opt>)\n\ +\ -fnone Turn off all language support options above\n" ^ + debugging_help ^ +"Optimization options: (use -fno-<opt> to turn off -f<opt>)\n\ \ -O Optimize the compiled code [on by default]\n\ \ -O0 Do not optimize the compiled code\n\ \ -O1 -O2 -O3 Synonymous for -O\n\ @@ -346,32 +385,13 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>)\n\ \ -fsmall-const <n> Set maximal size <n> for allocation in small constant area\n\ \ -falign-functions <n> Set alignment (in bytes) of function entry points\n\ \ -falign-branch-targets <n> Set alignment (in bytes) of branch targets\n\ -\ -falign-cond-branches <n> Set alignment (in bytes) of conditional branches\n\ -Target processor options:\n\ -\ -mthumb (ARM only) Use Thumb2 instruction encoding\n\ -\ -marm (ARM only) Use classic ARM instruction encoding\n\ -Assembling options:\n\ +\ -falign-cond-branches <n> Set alignment (in bytes) of conditional branches\n" ^ + target_help ^ +"Assembling options:\n\ \ -Wa,<opt> Pass option <opt> to the assembler\n\ -\ -Xassembler <opt> Pass <opt> as an option to the assembler\n\ -Linking options:\n\ -\ -l<lib> Link library <lib>\n\ -\ -L<dir> Add <dir> to search path for libraries\n\ -\ -nostartfiles (GCC only) Do not use the standard system startup files when\n\ -\ linking\n\ -\ -nodefaultlibs (GCC only) Do not use the standard system libraries when\n\ -\ linking\n\ -\ -nostdlib (GCC only) Do not use the standard system startup files or\n\ -\ libraries when linking\n\ -\ -s Remove all symbol table and relocation information from the\n\ -\ executable\n\ -\ -static Prevent linking with the shared libraries\n\ -\ -T <file> Use <file> as linker command file\n\ -\ -Wl,<opt> Pass option <opt> to the linker\n\ -\ -WUl,<opt> (GCC only) Pass option <opt> to the gcc used for linking\n\ -\ -Xlinker <opt> Pass <opt> as an option to the linker\n\ -\ -u <symb> Pretend the symbol <symb> is undefined to force linking of\n\ -\ library modules to define it.\n\ -Tracing options:\n\ +\ -Xassembler <opt> Pass <opt> as an option to the assembler\n" ^ + linker_help ^ +"Tracing options:\n\ \ -dprepro Save C file after preprocessing in <file>.i\n\ \ -dparse Save C file after parsing and elaboration in <file>.parsed.c\n\ \ -dc Save generated Compcert C in <file>.compcert.c\n\ @@ -414,10 +434,6 @@ let optimization_options = [ let set_all opts = List.iter (fun r -> r := true) opts let unset_all opts = List.iter (fun r -> r := false) opts -let gnu_linker_opt s = - if gnu_option s then - push_linker_arg s - let num_source_files = ref 0 let num_input_files = ref 0 @@ -446,12 +462,13 @@ let cmdline_actions = Exact "-fnone", Self (fun _ -> unset_all language_support_options); (* Debugging options *) Exact "-g", Self (fun s -> option_g := true; - option_gdwarf := 3); - Exact "-gdwarf-2", Self (fun s -> option_g:=true; + option_gdwarf := 3);] @ + if gnu_system then + [ Exact "-gdwarf-2", Self (fun s -> option_g:=true; option_gdwarf := 2); Exact "-gdwarf-3", Self (fun s -> option_g := true; - option_gdwarf := 3); - Exact "-frename-static", Self (fun s -> option_rename_static:= true); + option_gdwarf := 3);] else [] @ + [ Exact "-frename-static", Self (fun s -> option_rename_static:= true); Exact "-gdepth", Integer (fun n -> if n = 0 || n <0 then begin option_g := false end else begin @@ -471,32 +488,35 @@ let cmdline_actions = Exact "-falign-cond-branches", Integer(fun n -> option_faligncondbranchs := n); (* Target processor options *) Exact "-conf", String (fun _ -> ()); (* Ignore option since it is already handled *) - Exact "-target", String (fun _ -> ()); (* Ignore option since it is already handled *) - Exact "-mthumb", Set option_mthumb; - Exact "-marm", Unset option_mthumb; + Exact "-target", String (fun _ -> ());] @ (* Ignore option since it is already handled *) + if Configuration.arch = "arm" then + [ Exact "-mthumb", Set option_mthumb; + Exact "-marm", Unset option_mthumb; ] + else [] @ (* Assembling options *) - Prefix "-Wa,", Self (fun s -> if Configuration.system = "diab" then - assembler_options := List.rev_append (explode_comma_option s) !assembler_options + [ Prefix "-Wa,", Self (fun s -> if gnu_system then + assembler_options := s :: !assembler_options else - assembler_options := s :: !assembler_options); - Exact "-Xassembler", String (fun s -> if Configuration.system = "diab" then - assembler_options := s::!assembler_options + assembler_options := List.rev_append (explode_comma_option s) !assembler_options); + Exact "-Xassembler", String (fun s -> if gnu_system then + assembler_options := s::"-Xassembler":: !assembler_options else - assembler_options := s::"-Xassembler":: !assembler_options); + assembler_options := s::!assembler_options ); (* Linking options *) Prefix "-l", Self push_linker_arg; - Prefix "-L", Self push_linker_arg; - Exact "-nostartfiles", Self gnu_linker_opt; - Exact "-nodefaultlibs", Self gnu_linker_opt; - Exact "-nostdlib", Self gnu_linker_opt; - Exact "-s", Self push_linker_arg; + Prefix "-L", Self push_linker_arg; ] @ + if gnu_system then + [ Exact "-nostartfiles", Self push_linker_arg; + Exact "-nodefaultlibs", Self push_linker_arg; + Exact "-nostdlib", Self push_linker_arg;] + else [] @ + [ Exact "-s", Self push_linker_arg; Exact "-static", Self push_linker_arg; - Exact "-T", String (fun s -> if Configuration.system = "diab" then - push_linker_arg ("-Wm"^s) - else begin - push_linker_arg ("-T"); - push_linker_arg(s) - end); + Exact "-T", String (fun s -> if gnu_system then begin + push_linker_arg ("-T"); + push_linker_arg(s) + end else + push_linker_arg ("-Wm"^s)); Exact "-Xlinker", String (fun s -> if Configuration.system = "diab" then push_linker_arg ("-Wl,"^s) else diff --git a/driver/Frontend.ml b/driver/Frontend.ml index 44ad1700..00387a05 100644 --- a/driver/Frontend.ml +++ b/driver/Frontend.ml @@ -82,36 +82,18 @@ let parse_c_file sourcename ifile = (* Add gnu preprocessor list *) let gnu_prepro_opt_key key s = - if gnu_option s then - prepro_options := s::key::!prepro_options + prepro_options := s::key::!prepro_options (* Add gnu preprocessor option *) let gnu_prepro_opt s = - if gnu_option s then - prepro_options := s::!prepro_options + prepro_options := s::!prepro_options (* Add gnu preprocessor option s and the implict -E *) let gnu_prepro_opt_e s = - if gnu_option s then begin - prepro_options := s :: !prepro_options; - option_E := true - end + prepro_options := s :: !prepro_options; + option_E := true -let prepro_actions = [ - (* Preprocessing options *) - Exact "-I", String(fun s -> prepro_options := s :: "-I" :: !prepro_options; - assembler_options := s :: "-I" :: !assembler_options); - Prefix "-I", Self(fun s -> prepro_options := s :: !prepro_options; - assembler_options := s :: !assembler_options); - Exact "-D", String(fun s -> prepro_options := s :: "-D" :: !prepro_options); - Prefix "-D", Self(fun s -> prepro_options := s :: !prepro_options); - Exact "-U", String(fun s -> prepro_options := s :: "-U" :: !prepro_options); - Prefix "-U", Self(fun s -> prepro_options := s :: !prepro_options); - Prefix "-Wp,", Self (fun s -> - prepro_options := List.rev_append (explode_comma_option s) !prepro_options); - Exact "-Xpreprocessor", String (fun s -> - prepro_options := s :: !prepro_options); - Exact "-include", String (fun s -> prepro_options := s :: "-include" :: !prepro_options); +let gnu_prepro_actions = [ Exact "-M", Self gnu_prepro_opt_e; Exact "-MM", Self gnu_prepro_opt_e; Exact "-MF", String (gnu_prepro_opt_key "-MF"); @@ -128,36 +110,55 @@ let prepro_actions = [ Exact "-C", Self gnu_prepro_opt; Exact "-CC", Self gnu_prepro_opt;] -let prepro_help = "Preprocessing options:\n\ -\ -I<dir> Add <dir> to search path for #include files\n\ -\ -include <file> Process <file> as if #include \"<file>\" appears at the first\n\ -\ line of the primary source file.\n\ -\ -D<symb>=<val> Define preprocessor symbol\n\ -\ -U<symb> Undefine preprocessor symbol\n\ -\ -Wp,<opt> Pass option <opt> to the preprocessor\n\ -\ -Xpreprocessor <opt> Pass option <opt> to the preprocessor\n\ -\ -M (GCC only) Ouput a rule suitable for make describing the\n\ +let prepro_actions = [ + (* Preprocessing options *) + Exact "-I", String(fun s -> prepro_options := s :: "-I" :: !prepro_options; + assembler_options := s :: "-I" :: !assembler_options); + Prefix "-I", Self(fun s -> prepro_options := s :: !prepro_options; + assembler_options := s :: !assembler_options); + Exact "-D", String(fun s -> prepro_options := s :: "-D" :: !prepro_options); + Prefix "-D", Self(fun s -> prepro_options := s :: !prepro_options); + Exact "-U", String(fun s -> prepro_options := s :: "-U" :: !prepro_options); + Prefix "-U", Self(fun s -> prepro_options := s :: !prepro_options); + Prefix "-Wp,", Self (fun s -> + prepro_options := List.rev_append (explode_comma_option s) !prepro_options); + Exact "-Xpreprocessor", String (fun s -> + prepro_options := s :: !prepro_options); + Exact "-include", String (fun s -> prepro_options := s :: "-include" :: !prepro_options);] + @ (if Configuration.system <> "diab" then gnu_prepro_actions else []) + +let gnu_prepro_help = +"\ -M Ouput a rule suitable for make describing the\n\ \ dependencies of the main source file\n\ -\ -MM (GCC only) Like -M but do not mention system header files\n\ -\ -MF <file> (GCC only) Specifies file <file> as output file for -M or -MM\n\ -\ -MG (GCC only) Assumes missing header files are generated for -M\n\ -\ -MP (GCC only) Add a phony target for each dependency other than\n\ +\ -MM Like -M but do not mention system header files\n\ +\ -MF <file> Specifies file <file> as output file for -M or -MM\n\ +\ -MG Assumes missing header files are generated for -M\n\ +\ -MP Add a phony target for each dependency other than\n\ \ the main file\n\ -\ -MT <target> (GCC only) Change the target of the rule emitted by dependency\n\ +\ -MT <target> Change the target of the rule emitted by dependency\n\ \ generation\n\ -\ -MQ <target> (GCC only) Like -MT but quotes <target>\n\ -\ -nostdinc (GCC only) Do not search the standard system directories for\n\ +\ -MQ <target> Like -MT but quotes <target>\n\ +\ -nostdinc Do not search the standard system directories for\n\ \ header files\n\ -\ -imacros <file> (GCC only) Like -include but throws output produced by\n\ +\ -imacros <file> Like -include but throws output produced by\n\ \ preprocessing of <file> away\n\ -\ -idirafter <dir> (GCC only) Search <dir> for header files after all directories\n\ +\ -idirafter <dir> Search <dir> for header files after all directories\n\ \ specified with -I and the standard system directories\n\ -\ -isystem <dir> (GCC only) Search <dir> for header files after all directories\n\ -\ +\ -isystem <dir> Search <dir> for header files after all directories\n\ \ specified by -I but before the standard system directories\n\ -\ -iquote <dir> (GCC only) Like -isystem but only for headers included with\n\ -\ quotes\n\ -\ -P (GCC only) Do not generate linemarkers\n\ -\ -C (GCC only) Do not discard comments\n\ -\ -CC (GCC only) Do not discard comments, including during macro\n\ +\ -iquote <dir> Like -isystem but only for headers included with\n\ +\ quotes\n\ +\ -P Do not generate linemarkers\n\ +\ -C Do not discard comments\n\ +\ -CC Do not discard comments, including during macro\n\ \ expansion\n" + +let prepro_help = "Preprocessing options:\n\ +\ -I<dir> Add <dir> to search path for #include files\n\ +\ -include <file> Process <file> as if #include \"<file>\" appears at the first\n\ +\ line of the primary source file.\n\ +\ -D<symb>=<val> Define preprocessor symbol\n\ +\ -U<symb> Undefine preprocessor symbol\n\ +\ -Wp,<opt> Pass option <opt> to the preprocessor\n\ +\ -Xpreprocessor <opt> Pass option <opt> to the preprocessor\n" + ^ (if Configuration.system <> "diab" then gnu_prepro_help else "") |