diff options
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Configuration.mli | 11 | ||||
| -rw-r--r-- | driver/Driver.ml | 18 | ||||
| -rw-r--r-- | driver/Interp.ml | 21 |
3 files changed, 29 insertions, 21 deletions
diff --git a/driver/Configuration.mli b/driver/Configuration.mli index 1d048ac4..abfd3ab4 100644 --- a/driver/Configuration.mli +++ b/driver/Configuration.mli @@ -12,27 +12,37 @@ val arch: string (** Target architecture *) + val model: string (** Sub-model for this architecture *) + val abi: string (** ABI to use *) + val system: string (** Flavor of operating system that runs CompCert *) val prepro: string list (** How to invoke the external preprocessor *) + val asm: string list (** How to invoke the external assembler *) + val linker: string list (** How to invoke the external linker *) + val asm_supports_cfi: bool (** True if the assembler supports Call Frame Information *) + val stdlib_path: string (** Path to CompCert's library *) + val has_runtime_lib: bool (** True if CompCert's library is available. *) + val has_standard_headers: bool (** True if CompCert's standard header files is available. *) + val advanced_debug: bool (** True if advanced debug is implement for the Target *) @@ -52,6 +62,7 @@ type struct_return_style = val struct_passing_style: struct_passing_style (** Calling conventions to use for passing structs and unions as first-class values *) + val struct_return_style: struct_return_style (** Calling conventions to use for returning structs and unions as first-class values *) diff --git a/driver/Driver.ml b/driver/Driver.ml index bbd949e0..16267128 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -159,7 +159,7 @@ let parse_c_file sourcename ifile = PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax; close_out oc end; - csyntax,None + csyntax (* Dump Asm code in asm format for the validator *) @@ -174,7 +174,7 @@ let dump_jasm asm sourcename destfile = (* From CompCert C AST to asm *) -let compile_c_ast sourcename csyntax ofile debug = +let compile_c_ast sourcename csyntax ofile = (* Prepare to dump Clight, RTL, etc, if requested *) let set_dest dst opt ext = dst := if !opt then Some (output_filename sourcename ".c" ext) @@ -200,14 +200,14 @@ let compile_c_ast sourcename csyntax ofile debug = dump_jasm asm sourcename (output_filename sourcename ".c" !sdump_suffix); (* Print Asm in text form *) let oc = open_out ofile in - PrintAsm.print_program oc asm debug; + PrintAsm.print_program oc asm; close_out oc (* From C source to asm *) let compile_c_file sourcename ifile ofile = - let ast,debug = parse_c_file sourcename ifile in - compile_c_ast sourcename ast ofile debug + let ast = parse_c_file sourcename ifile in + compile_c_ast sourcename ast ofile (* From Cminor to asm *) @@ -232,7 +232,7 @@ let compile_cminor_file ifile ofile = exit 2 | Errors.OK p -> let oc = open_out ofile in - PrintAsm.print_program oc p None; + PrintAsm.print_program oc p; close_out oc with Parsing.Parse_error -> eprintf "File %s, character %d: Syntax error\n" @@ -304,7 +304,7 @@ let process_c_file sourcename = let name = if !option_interp then begin Machine.config := Machine.compcert_interpreter !Machine.config; - let csyntax,_ = parse_c_file sourcename preproname in + let csyntax = parse_c_file sourcename preproname in if not !option_dprepro then safe_remove preproname; Interp.execute csyntax; @@ -338,7 +338,7 @@ let process_c_file sourcename = let process_i_file sourcename = ensure_inputfile_exists sourcename; if !option_interp then begin - let csyntax,_ = parse_c_file sourcename sourcename in + let csyntax = parse_c_file sourcename sourcename in Interp.execute csyntax; "" end else if !option_S then begin @@ -438,7 +438,7 @@ let perform_actions () = let explode_comma_option s = match Str.split (Str.regexp ",") s with | [] -> assert false - | hd :: tl -> tl + | _ :: tl -> tl let version_string = if Version.buildnr <> "" && Version.tag <> "" then diff --git a/driver/Interp.ml b/driver/Interp.ml index 4b6d0a44..5c2158ae 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -12,20 +12,17 @@ (* Interpreting CompCert C sources *) -open Format +open !Format open Camlcoq -open Datatypes open AST open Integers open Values open Memory open Globalenvs open Events -open Ctypes -open Cop -open Csyntax +open !Ctypes +open !Csyntax open Csem -open Clflags (* Configuration *) @@ -86,16 +83,16 @@ let name_of_fundef prog fd = if fd == fd' then extern_atom id else find_name rem | (id, Gvar v) :: rem -> find_name rem - in find_name prog.prog_defs + in find_name prog.Ctypes.prog_defs let name_of_function prog fn = let rec find_name = function | [] -> "<unknown function>" - | (id, Gfun(Internal fn')) :: rem -> + | (id, Gfun(Ctypes.Internal fn')) :: rem -> if fn == fn' then extern_atom id else find_name rem | (id, _) :: rem -> find_name rem - in find_name prog.prog_defs + in find_name prog.Ctypes.prog_defs let invert_local_variable e b = Maps.PTree.fold @@ -584,7 +581,7 @@ let world_program prog = (id, Gvar gv') | Gfun fd -> (id, gd) in - {prog with prog_defs = List.map change_def prog.prog_defs} + {prog with Ctypes.prog_defs = List.map change_def prog.Ctypes.prog_defs} (* Massaging the program to get a suitable "main" function *) @@ -599,7 +596,7 @@ let change_main_function p old_main old_main_ty = fn_params = []; fn_vars = []; fn_body = body } in let new_main_id = intern_string "___main" in { prog_main = new_main_id; - prog_defs = (new_main_id, Gfun(Internal new_main_fn)) :: p.prog_defs; + Ctypes.prog_defs = (new_main_id, Gfun(Internal new_main_fn)) :: p.Ctypes.prog_defs; prog_public = p.prog_public; prog_types = p.prog_types; prog_comp_env = p.prog_comp_env } @@ -610,7 +607,7 @@ let rec find_main_function name = function | (id, Gvar v) :: gdl -> find_main_function name gdl let fixup_main p = - match find_main_function p.prog_main p.prog_defs with + match find_main_function p.Ctypes.prog_main p.prog_defs with | None -> fprintf err_formatter "ERROR: no main() function@."; None |