From 8a95c3e07fd02eaa87f8cca447bc7d7c2642eb22 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 16 Oct 2015 15:19:24 +0200 Subject: Do not dump the .sdump files. Bug 16529. --- driver/Driver.ml | 17 ++--------------- 1 file changed, 2 insertions(+), 15 deletions(-) (limited to 'driver/Driver.ml') diff --git a/driver/Driver.ml b/driver/Driver.ml index 7459e030..8fe6b07d 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -144,17 +144,7 @@ let parse_c_file sourcename ifile = end; csyntax,None -(* Dump Asm code in binary format for the validator *) - -let sdump_magic_number = "CompCertSDUMP" ^ Version.version - -let dump_asm asm destfile = - let oc = open_out_bin destfile in - output_string oc sdump_magic_number; - output_value oc asm; - output_value oc Camlcoq.string_of_atom; - output_value oc C2C.decl_atom; - close_out oc +(* Dump Asm code in asm format for the validator *) let jdump_magic_number = "CompCertJDUMP" ^ Version.version @@ -190,10 +180,7 @@ let compile_c_ast sourcename csyntax ofile debug = exit 2 in (* Dump Asm in binary and JSON format *) if !option_sdump then - begin - dump_asm asm (output_filename sourcename ".c" ".sdump"); - dump_jasm asm (output_filename sourcename ".c" ".json") - end; + dump_jasm asm (output_filename sourcename ".c" ".json"); (* Print Asm in text form *) let oc = open_out ofile in PrintAsm.print_program oc asm debug; -- cgit