diff options
| author | Alasdair Armstrong | 2018-01-24 17:44:22 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-01-24 19:53:05 +0000 |
| commit | 10e2be330c14aaddbd8ada6b6ce8a8a63c7d605e (patch) | |
| tree | ac904feb95f86f0758b74804e632b4785b601acc /src/sail.ml | |
| parent | cd81acaf58db3edc4187e4cccc35f6aa76d6933d (diff) | |
Have some simple sail programs compiling to C
Diffstat (limited to 'src/sail.ml')
| -rw-r--r-- | src/sail.ml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/sail.ml b/src/sail.ml index 00f90d3b..b819350b 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -60,6 +60,7 @@ let opt_print_verbose = ref false let opt_print_lem_ast = ref false let opt_print_lem = ref false let opt_print_ocaml = ref false +let opt_print_c = ref false let opt_memo_z3 = ref false let opt_sanity = ref false let opt_libs_lem = ref ([]:string list) @@ -83,6 +84,9 @@ let options = Arg.align ([ ( "-ocaml_trace", Arg.Tuple [Arg.Set opt_print_ocaml; Arg.Set Initial_check.opt_undefined_gen; Arg.Set Ocaml_backend.opt_trace_ocaml], " output an OCaml translated version of the input with tracing instrumentation, implies -ocaml"); + ( "-c", + Arg.Tuple [Arg.Set opt_print_c; (* Arg.Set Initial_check.opt_undefined_gen *)], + " output a C translated version of the input"); ( "-lem_ast", Arg.Set opt_print_lem_ast, " output a Lem AST representation of the input"); @@ -242,6 +246,11 @@ let main() = let out = match !opt_file_out with None -> "out" | Some s -> s in Ocaml_backend.ocaml_compile out ast_ocaml else ()); + (if !(opt_print_c) + then + let ast_c = rewrite_ast_c ast in + C_backend.compile_ast type_envs ast_c + else ()); (if !(opt_print_lem) then let ast_lem = rewrite_ast_lem ast in output "" (Lem_out (!opt_libs_lem)) [out_name,ast_lem] |