diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-03-18 18:36:09 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-03-18 18:36:09 +0100 |
| commit | f750e0ac9ee99072cca8361f591015f1f82681fa (patch) | |
| tree | 52f702c00806e01e3ea675d880c08fcb3b9322c1 /driver | |
| parent | 89e7840807d9b39636ed84c43ec21485ea776cf9 (diff) | |
| download | compcert-f750e0ac9ee99072cca8361f591015f1f82681fa.tar.gz compcert-f750e0ac9ee99072cca8361f591015f1f82681fa.zip | |
Added function to convert C types into their dwarf represnation.
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Driver.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index d8b28285..f14b2671 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -15,6 +15,7 @@ open Commandline open Camlcoq open Clflags open Timing +open CtoDwarf (* Location of the compatibility library *) @@ -181,7 +182,7 @@ let compile_c_ast sourcename csyntax ofile = dump_asm asm (output_filename sourcename ".c" ".sdump"); (* Print Asm in text form *) let oc = open_out ofile in - PrintAsm.print_program oc asm; + PrintAsm.print_program oc asm None; close_out oc (* From C source to asm *) @@ -212,7 +213,7 @@ let compile_cminor_file ifile ofile = exit 2 | Errors.OK p -> let oc = open_out ofile in - PrintAsm.print_program oc p; + PrintAsm.print_program oc p None; close_out oc with Parsing.Parse_error -> eprintf "File %s, character %d: Syntax error\n" |