Deactivate options target dependend.

Options only available for gnu systems or arm target arch are no
longer displayed in the help and cannot be selected any longer.
Bug 19197

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 "")