aboutsummaryrefslogtreecommitdiffstats
path: root/driver
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-03-24 16:07:45 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2015-03-24 16:07:45 +0100
commit2ebf8bfda476966209d681470ebe6301fb10db0a (patch)
tree15bc824d8c92a5d089852a3a21648cba7af242eb /driver
parent275d7f4091609ae30093a4a83a20a74997229f9c (diff)
downloadcompcert-2ebf8bfda476966209d681470ebe6301fb10db0a.tar.gz
compcert-2ebf8bfda476966209d681470ebe6301fb10db0a.zip
Added missing functions for printing the structs and unions. Still missing printing of packed structs.
Diffstat (limited to 'driver')
-rw-r--r--driver/Driver.ml12
1 files changed, 4 insertions, 8 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 80a5891c..1191982d 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -15,7 +15,6 @@ open Commandline
open Camlcoq
open Clflags
open Timing
-open CtoDwarf
(* Location of the compatibility library *)
@@ -118,20 +117,17 @@ let parse_c_file sourcename ifile =
^ (if !option_fpacked_structs then "p" else "")
in
(* Parsing and production of a simplified C AST *)
- let ast =
+ let ast,debug =
match Parse.preprocessed_file simplifs sourcename ifile with
- | None -> exit 2
- | Some p -> p in
+ | None,_ -> exit 2
+ | Some p,d -> p,d in
(* Save C AST if requested *)
if !option_dparse then begin
let ofile = output_filename sourcename ".c" ".parsed.c" in
let oc = open_out ofile in
Cprint.program (Format.formatter_of_out_channel oc) ast;
close_out oc
- end;
- let debug = if !option_g && Configuration.advanced_debug then
- Some (program_to_dwarf ast sourcename)
- else None in
+ end;
(* Conversion to Csyntax *)
let csyntax =
match Timing.time "CompCert C generation" C2C.convertProgram ast with