aboutsummaryrefslogtreecommitdiffstats
path: root/driver
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-09-16 11:10:28 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2015-09-16 11:10:28 +0200
commit3344bcf59acb1ae8d43a0d15acb4b824689e706d (patch)
treea5621a5d30ee7e39e2e6d2a95e02ab018e8ef846 /driver
parent36fe88d4cc2022947474a2fcc0b650e22f41ee3e (diff)
downloadcompcert-3344bcf59acb1ae8d43a0d15acb4b824689e706d.tar.gz
compcert-3344bcf59acb1ae8d43a0d15acb4b824689e706d.zip
Add the debug interface file.
The new file Debug.ml contains the interface for generating and printing debug information. In order to generate debug information the init function initializes the necessary functions depending on the -g flag. If the -g is not there all functions are dummy functions which do nothing.
Diffstat (limited to 'driver')
-rw-r--r--driver/Driver.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml
index f53de821..04acf902 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -682,6 +682,7 @@ let _ =
Builtins.set C2C.builtins;
CPragmas.initialize();
parse_cmdline cmdline_actions;
+ Debug.init (); (* Initialize the debug functions *)
let nolink = !option_c || !option_S || !option_E || !option_interp in
if nolink && !option_o <> None && !num_source_files >= 2 then begin
eprintf "Ambiguous '-o' option (multiple source files)\n";