diff options
| -rw-r--r-- | src/c_backend.ml | 9 | ||||
| -rw-r--r-- | src/c_backend.mli | 2 | ||||
| -rw-r--r-- | src/sail.ml | 6 |
3 files changed, 11 insertions, 6 deletions
diff --git a/src/c_backend.ml b/src/c_backend.ml index 8c5658e7..61e8777e 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -3009,7 +3009,7 @@ let rec get_recursive_functions (Defs defs) = | _ :: defs -> get_recursive_functions (Defs defs) | [] -> IdSet.empty -let compile_ast ctx (Defs defs) = +let compile_ast ctx c_includes (Defs defs) = try c_debug (lazy (Util.log_line __MODULE__ __LINE__ "Identifying recursive functions")); let recursive_functions = Spec_analysis.top_sort_defs (Defs defs) |> get_recursive_functions in @@ -3030,9 +3030,10 @@ let compile_ast ctx (Defs defs) = let docs = List.map (codegen_def ctx) cdefs in let preamble = separate hardline - [ string "#include \"sail.h\""; - string "#include \"rts.h\""; - string "#include \"elf.h\"" ] + ([ string "#include \"sail.h\""; + string "#include \"rts.h\""; + string "#include \"elf.h\"" ] + @ (List.map (fun h -> string (Printf.sprintf "#include \"%s\"" h)) c_includes)) in let exn_boilerplate = diff --git a/src/c_backend.mli b/src/c_backend.mli index 142a5ed5..6e175ad7 100644 --- a/src/c_backend.mli +++ b/src/c_backend.mli @@ -70,7 +70,7 @@ type ctx should be the environment returned by typechecking the full AST. *) val initial_ctx : Env.t -> ctx -val compile_ast : ctx -> tannot Ast.defs -> unit +val compile_ast : ctx -> string list -> tannot Ast.defs -> unit val bytecode_ast : ctx -> (cdef list -> cdef list) -> tannot Ast.defs -> cdef list diff --git a/src/sail.ml b/src/sail.ml index 12df5515..d7919dcb 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -66,6 +66,7 @@ let opt_print_latex = ref false let opt_print_coq = ref false let opt_memo_z3 = ref false let opt_sanity = ref false +let opt_includes_c = ref ([]:string list) let opt_libs_lem = ref ([]:string list) let opt_libs_coq = ref ([]:string list) let opt_file_arguments = ref ([]:string list) @@ -109,6 +110,9 @@ let options = Arg.align ([ ( "-c", Arg.Tuple [Arg.Set opt_print_c; Arg.Set Initial_check.opt_undefined_gen], " output a C translated version of the input"); + ( "-c_include", + Arg.String (fun i -> opt_includes_c := i::!opt_includes_c), + " <filename> provide additional include for C output"); ( "-elf", Arg.String (fun elf -> opt_process_elf := Some elf), " process an elf file so that it can be executed by compiled C code"); @@ -317,7 +321,7 @@ let main() = let ast_c = rewrite_ast_c ast in let ast_c, type_envs = Specialize.specialize ast_c type_envs in let ast_c = Spec_analysis.top_sort_defs ast_c in - C_backend.compile_ast (C_backend.initial_ctx type_envs) ast_c + C_backend.compile_ast (C_backend.initial_ctx type_envs) (!opt_includes_c) ast_c else ()); (if !(opt_print_lem) then |