diff options
| -rw-r--r-- | src/c_backend.ml | 13 | ||||
| -rw-r--r-- | src/c_backend.mli | 1 | ||||
| -rw-r--r-- | src/sail.ml | 5 |
3 files changed, 16 insertions, 3 deletions
diff --git a/src/c_backend.ml b/src/c_backend.ml index 94d29c21..57921e3f 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -64,6 +64,7 @@ let c_verbosity = ref 0 let opt_ddump_flow_graphs = ref false let opt_trace = ref false let opt_static = ref false +let opt_no_main = ref false (* Optimization flags *) let optimize_primops = ref false @@ -3094,8 +3095,8 @@ let compile_ast ctx c_includes (Defs defs) = "}" ] )) in - let model_main = separate hardline (List.map string - [ "int main(int argc, char *argv[])"; + let model_default_main = separate hardline (List.map string + [ "int model_main(int argc, char *argv[])"; "{"; " model_init();"; " if (process_arguments(argc, argv)) exit(EXIT_FAILURE);"; @@ -3105,11 +3106,19 @@ let compile_ast ctx c_includes (Defs defs) = "}" ] ) in + let model_main = separate hardline (if (!opt_no_main) then [] else List.map string + [ "int main(int argc, char *argv[])"; + "{"; + " return model_main(argc, argv);"; + "}" ] ) + in + let hlhl = hardline ^^ hardline in Pretty_print_sail.to_string (preamble ^^ hlhl ^^ separate hlhl docs ^^ hlhl ^^ model_init ^^ hlhl ^^ model_fini ^^ hlhl + ^^ model_default_main ^^ hlhl ^^ model_main) |> print_endline with diff --git a/src/c_backend.mli b/src/c_backend.mli index 6e175ad7..170c5bd9 100644 --- a/src/c_backend.mli +++ b/src/c_backend.mli @@ -56,6 +56,7 @@ open Type_check val opt_ddump_flow_graphs : bool ref val opt_trace : bool ref val opt_static : bool ref +val opt_no_main : bool ref (** Optimization flags *) diff --git a/src/sail.ml b/src/sail.ml index d7919dcb..de186be9 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -103,7 +103,7 @@ let options = Arg.align ([ " set a custom directory to build generated OCaml"); ( "-ocaml-coverage", Arg.Set Ocaml_backend.opt_ocaml_coverage, - "Build ocaml with bisect_ppx coverage reporting (requires opam packages bisect_ppx-ocamlbuild and bisect_ppx)."); + " Build ocaml with bisect_ppx coverage reporting (requires opam packages bisect_ppx-ocamlbuild and bisect_ppx)."); ( "-latex", Arg.Set opt_print_latex, " pretty print the input to latex"); @@ -113,6 +113,9 @@ let options = Arg.align ([ ( "-c_include", Arg.String (fun i -> opt_includes_c := i::!opt_includes_c), " <filename> provide additional include for C output"); + ( "-c_no_main", + Arg.Set C_backend.opt_no_main, + " do not generate the main() function" ); ( "-elf", Arg.String (fun elf -> opt_process_elf := Some elf), " process an elf file so that it can be executed by compiled C code"); |