diff options
| author | Alasdair Armstrong | 2018-12-13 16:20:48 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-12-13 16:20:48 +0000 |
| commit | b167a59affdb6428fa0656a092b335a3a6899d56 (patch) | |
| tree | f8b5a9d7a11bd1753d2861653841448db8f7cb07 /src/sail.ml | |
| parent | f19023bedee7b32a39b23907b0a1cd732a1e3bc9 (diff) | |
Add hooks to call cgen stub file for RISC-V
Diffstat (limited to 'src/sail.ml')
| -rw-r--r-- | src/sail.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/sail.ml b/src/sail.ml index 73173946..0d26df9c 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -64,6 +64,7 @@ let opt_print_ocaml = ref false let opt_print_c = ref false let opt_print_latex = ref false let opt_print_coq = ref false +let opt_print_cgen = ref false let opt_memo_z3 = ref false let opt_sanity = ref false let opt_includes_c = ref ([]:string list) @@ -143,6 +144,9 @@ let options = Arg.align ([ ( "-trace", Arg.Tuple [Arg.Set C_backend.opt_trace; Arg.Set Ocaml_backend.opt_trace_ocaml], " Instrument ouput with tracing"); + ( "-cgen", + Arg.Set opt_print_cgen, + " Generate CGEN source"); ( "-lem", Arg.Set opt_print_lem, " output a Lem translated version of the input"); @@ -352,6 +356,9 @@ let main() = Util.opt_warnings := true; C_backend.compile_ast (C_backend.initial_ctx type_envs) (!opt_includes_c) ast_c else ()); + (if !(opt_print_cgen) + then Cgen_backend.output type_envs ast + else ()); (if !(opt_print_lem) then let mwords = !Pretty_print_lem.opt_mwords in |