diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-05-17 08:18:07 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-05-17 08:18:07 +0000 |
| commit | f692ee29c1ea8748120ca1a4cbb4cd7f1eb2531e (patch) | |
| tree | 9cc9ccd22b5010ef9d16e9a2a1017741d0ff6e13 /driver | |
| parent | 807d49a50b126bd1013de110128cfe2ac22f02dc (diff) | |
Preliminary support for debugging info (-g).
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2253 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Clflags.ml | 1 | ||||
| -rw-r--r-- | driver/Driver.ml | 20 |
2 files changed, 13 insertions, 8 deletions
diff --git a/driver/Clflags.ml b/driver/Clflags.ml index ea8e884..d70467a 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -40,6 +40,7 @@ let option_dalloctrace = ref false let option_dmach = ref false let option_dasm = ref false let option_sdump = ref false +let option_g = ref false let option_o = ref (None: string option) let option_E = ref false let option_S = ref false diff --git a/driver/Driver.ml b/driver/Driver.ml index e029aa2..3d981f0 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -396,6 +396,12 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>) : -falign-branch-targets <n> Set alignment (in bytes) of branch targets -falign-cond-branches <n> Set alignment (in bytes) of conditional branches -Wa,<opt> Pass option <opt> to the assembler +Debugging options: + -g Generate debugging information +Linking options: + -l<lib> Link library <lib> + -L<dir> Add <dir> to search path for libraries + -Wl,<opt> Pass option <opt> to the linker Tracing options: -dparse Save C file after parsing and elaboration in <file>.parse.c -dc Save generated Compcert C in <file>.compcert.c @@ -410,10 +416,6 @@ Tracing options: -dmach Save generated Mach code in <file>.mach -dasm Save generated assembly in <file>.s -sdump Save info for post-linking validation in <file>.sdump -Linking options: - -l<lib> Link library <lib> - -L<dir> Add <dir> to search path for libraries - -Wl,<opt> Pass option <opt> to the linker General options: -stdlib <dir> Set the path of the Compcert run-time library -v Print external commands before invoking them @@ -441,6 +443,12 @@ let cmdline_actions = "-[IDU].", Self(fun s -> prepro_options := s :: !prepro_options); "-[lL].", Self(fun s -> linker_options := s :: !linker_options); "-o$", String(fun s -> option_o := Some s); + "-E$", Set option_E; + "-S$", Set option_S; + "-c$", Set option_c; + "-v$", Set option_v; + "-g$", Self (fun s -> + option_g := true; linker_options := s :: !linker_options); "-stdlib$", String(fun s -> stdlib_path := s); "-dparse$", Set option_dparse; "-dc$", Set option_dcmedium; @@ -456,10 +464,6 @@ let cmdline_actions = "-dmach$", Set option_dmach; "-dasm$", Set option_dasm; "-sdump$", Set option_sdump; - "-E$", Set option_E; - "-S$", Set option_S; - "-c$", Set option_c; - "-v$", Set option_v; "-interp$", Set option_interp; "-quiet$", Self (fun _ -> Interp.trace := 0); "-trace$", Self (fun _ -> Interp.trace := 2); |