diff options
| -rw-r--r--[-rwxr-xr-x] | driver/Driver.ml | 15 | ||||
| -rw-r--r-- | driver/Optionsprinter.ml | 141 |
2 files changed, 1 insertions, 155 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index 9d5ed3b3..1a6c47d5 100755..100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -19,8 +19,6 @@ open Frontend open Assembler open Linker -let dump_options = ref false - (* Optional sdump suffix *) let sdump_suffix = ref ".json" let sdump_folder = ref "" @@ -160,8 +158,6 @@ let process_c_file sourcename = if not !option_dasm then safe_remove asmname; objname end in - if !dump_options then - Optionsprinter.print (output_filename sourcename ".c" ".opt.json") !stdlib_path; name end @@ -176,8 +172,6 @@ let process_i_file sourcename = end else if !option_S then begin compile_c_file sourcename sourcename (output_filename ~final:true sourcename ".c" ".s"); - if !dump_options then - Optionsprinter.print (output_filename sourcename ".c" ".opt.json") !stdlib_path; "" end else begin let asmname = @@ -188,8 +182,6 @@ let process_i_file sourcename = let objname = output_filename ~final: !option_c sourcename ".c" ".o" in assemble asmname objname; if not !option_dasm then safe_remove asmname; - if !dump_options then - Optionsprinter.print (output_filename sourcename ".c" ".opt.json") !stdlib_path; objname end @@ -210,8 +202,6 @@ let process_cminor_file sourcename = let objname = output_filename ~final: !option_c sourcename ".cm" ".o" in assemble asmname objname; if not !option_dasm then safe_remove asmname; - if !dump_options then - Optionsprinter.print (output_filename sourcename ".cm" ".opt.json") !stdlib_path; objname end @@ -329,7 +319,6 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>) -dasm Save generated assembly in <file>.s -dall Save all generated intermediate files in <file>.<ext> -sdump Save info for post-linking validation in <file>.json - -doptions Save the compiler configurations in <file>.opt.json General options: -stdlib <dir> Set the path of the Compcert run-time library -v Print external commands before invoking them @@ -450,12 +439,10 @@ let cmdline_actions = option_drtl := true; option_dalloctrace := true; option_dmach := true; - option_dasm := true; - dump_options:=true); + option_dasm := true;); Exact "-sdump", Set option_sdump; Exact "-sdump-suffix", String (fun s -> option_sdump := true; sdump_suffix:= s); Exact "-sdump-folder", String (fun s -> sdump_folder := s); - Exact "-doptions", Set dump_options; (* General options *) Exact "-v", Set option_v; Exact "-stdlib", String(fun s -> stdlib_path := s); diff --git a/driver/Optionsprinter.ml b/driver/Optionsprinter.ml deleted file mode 100644 index 00b5f5ec..00000000 --- a/driver/Optionsprinter.ml +++ /dev/null @@ -1,141 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) -(* *) -(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *) -(* is distributed under the terms of the INRIA Non-Commercial *) -(* License Agreement. *) -(* *) -(* *********************************************************************) - -open Clflags -open Json -open Machine -open Printf - -let print_list oc name l = - p_jmember oc name (p_jarray p_jstring) l - -let print_clflags oc = - fprintf oc "{"; - print_list oc "prepro_options" !prepro_options; - print_list oc "linker_options" !linker_options; - print_list oc "assembler_options" !assembler_options; - p_jmember oc "flongdouble" p_jbool !option_flongdouble; - p_jmember oc "fstruct_passing" p_jbool !option_fstruct_passing; - p_jmember oc "fbitfields" p_jbool !option_fbitfields; - p_jmember oc "fvarag_calls" p_jbool !option_fvararg_calls; - p_jmember oc "funprototyped" p_jbool !option_funprototyped; - p_jmember oc "fpacked_structs" p_jbool !option_fpacked_structs; - p_jmember oc "ffpu" p_jbool !option_ffpu; - p_jmember oc "ffloatconstprop" p_jint !option_ffloatconstprop; - p_jmember oc "ftailcalls" p_jbool !option_ftailcalls; - p_jmember oc "fconstprop" p_jbool !option_fconstprop; - p_jmember oc "fcse" p_jbool !option_fcse; - p_jmember oc "fredundance" p_jbool !option_fredundancy; - p_jmember oc "falignfunctions" (p_jopt p_jint) !option_falignfunctions; - p_jmember oc "falignbranchtargets" p_jint !option_falignbranchtargets; - p_jmember oc "faligncondbranchs" p_jint !option_faligncondbranchs; - p_jmember oc "finline_asm" p_jbool !option_finline_asm; - p_jmember oc "mthumb" p_jbool !option_mthumb; - p_jmember oc "Osize" p_jbool !option_Osize; - p_jmember oc "dprepro" p_jbool !option_dprepro; - p_jmember oc "dparse" p_jbool !option_dparse; - p_jmember oc "dcmedium" p_jbool !option_dcmedium; - p_jmember oc "dclight" p_jbool !option_dclight; - p_jmember oc "dcminor" p_jbool !option_dcminor; - p_jmember oc "drtl" p_jbool !option_drtl; - p_jmember oc "dltl" p_jbool !option_dltl; - p_jmember oc "dalloctrace" p_jbool !option_dalloctrace; - p_jmember oc "dmach" p_jbool !option_dmach; - p_jmember oc "dasm" p_jbool !option_dasm; - p_jmember oc "sdump" p_jbool !option_sdump; - p_jmember oc "g" p_jbool !option_g; - p_jmember oc "gdwarf" p_jint !option_gdwarf; - p_jmember oc "gdepth" p_jint !option_gdepth; - p_jmember oc "o" (p_jopt p_jstring) !option_o; - p_jmember oc "E" p_jbool !option_E; - p_jmember oc "S" p_jbool !option_S; - p_jmember oc "c" p_jbool !option_c; - p_jmember oc "v" p_jbool !option_v; - p_jmember oc "interp" p_jbool !option_interp; - p_jmember oc "small_data" p_jint !option_small_data; - p_jmember oc "small_data" p_jint !option_small_const; - p_jmember oc "timings" p_jbool !option_timings; - fprintf oc "\n}" - -let print_struct_passing_style oc = function - | Configuration.SP_ref_callee -> p_jstring oc "SP_ref_callee" - | Configuration.SP_ref_caller -> p_jstring oc "SP_ref_caller" - | Configuration.SP_split_args -> p_jstring oc "SP_split_args" - -let print_struct_return_style oc = function - | Configuration.SR_int1248 -> p_jstring oc "SR_int1248" - | Configuration.SR_int1to4 -> p_jstring oc "SR_int1to4" - | Configuration.SR_int1to8 -> p_jstring oc "SR_int1to8" - | Configuration.SR_ref -> p_jstring oc "SR_ref" - -let print_configurations oc lib_path = - fprintf oc "{"; - p_jmember oc "arch" p_jstring Configuration.arch; - p_jmember oc "model" p_jstring Configuration.model; - p_jmember oc "abi" p_jstring Configuration.abi; - p_jmember oc "system" p_jstring Configuration.abi; - print_list oc "prepro" Configuration.prepro; - print_list oc "asm" Configuration.asm; - print_list oc "linker" Configuration.linker; - p_jmember oc "asm_supports_cfi" p_jbool Configuration.asm_supports_cfi; - p_jmember oc "stdlib_path" p_jstring lib_path; - p_jmember oc "has_runtime_lib" p_jbool Configuration.has_runtime_lib; - p_jmember oc "has_standard_headers" p_jbool Configuration.has_standard_headers; - p_jmember oc "struct_passing_style" print_struct_passing_style Configuration.struct_passing_style; - p_jmember oc "struct_return_style" print_struct_return_style Configuration.struct_return_style; - fprintf oc "\n}" - -let print_machine oc = - fprintf oc "{"; - p_jmember oc "name" p_jstring !config.name; - p_jmember oc "char_signed" p_jbool !config.char_signed; - p_jmember oc "sizeof_ptr" p_jint !config.sizeof_ptr; - p_jmember oc "sizeof_short" p_jint !config.sizeof_short; - p_jmember oc "sizeof_int" p_jint !config.sizeof_int; - p_jmember oc "sizeof_long" p_jint !config.sizeof_long; - p_jmember oc "sizeof_longlong" p_jint !config.sizeof_longlong; - p_jmember oc "sizeof_float" p_jint !config.sizeof_float; - p_jmember oc "sizeof_double" p_jint !config.sizeof_double; - p_jmember oc "sizeof_longdouble" p_jint !config.sizeof_longdouble; - p_jmember oc "sizeof_void" (p_jopt p_jint) !config.sizeof_void; - p_jmember oc "sizeof_fun" (p_jopt p_jint) !config.sizeof_fun; - p_jmember oc "sizeof_wchar" p_jint !config.sizeof_wchar; - p_jmember oc "wchar_signed" p_jbool !config.wchar_signed; - p_jmember oc "sizeof_size_t" p_jint !config.sizeof_size_t; - p_jmember oc "sizeof_ptrdiff_t" p_jint !config.sizeof_ptrdiff_t; - p_jmember oc "alignof_ptr" p_jint !config.alignof_ptr; - p_jmember oc "alignof_short" p_jint !config.alignof_short; - p_jmember oc "alignof_int" p_jint !config.alignof_int; - p_jmember oc "alignof_long" p_jint !config.alignof_long; - p_jmember oc "alignof_longlong" p_jint !config.alignof_longlong; - p_jmember oc "alignof_float" p_jint !config.alignof_float; - p_jmember oc "alignof_double" p_jint !config.alignof_double; - p_jmember oc "alignof_longdouble" p_jint !config.alignof_longdouble; - p_jmember oc "alignof_void" (p_jopt p_jint) !config.alignof_void; - p_jmember oc "alignof_fun" (p_jopt p_jint) !config.alignof_fun; - p_jmember oc "bigendian" p_jbool !config.bigendian; - p_jmember oc "bitfields_msb_first" p_jbool !config.bitfields_msb_first; - p_jmember oc "supports_unaligned_accesses" p_jbool !config.supports_unaligned_accesses; - fprintf oc "\n}" - -let print file stdlib = - let oc = open_out file in - fprintf oc "{"; - p_jmember oc "Version" p_jstring Version.version; - p_jmember oc "Buildnr" p_jstring Version.buildnr; - p_jmember oc "Tag" p_jstring Version.tag; - p_jmember oc "Cwd" p_jstring (Sys.getcwd ()); - fprintf oc "%a:%t" p_jstring "Clflags" print_clflags; - p_jmember oc "Configurations" print_configurations stdlib; - fprintf oc "%a:%t" p_jstring "Machine" print_machine; - fprintf oc "}"; - close_out oc |