diff options
Diffstat (limited to 'src/sail.ml')
| -rw-r--r-- | src/sail.ml | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/src/sail.ml b/src/sail.ml index 9c3a3d5c..95da54b0 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -124,6 +124,9 @@ let options = Arg.align ([ ( "-ir", set_target "ir", " print intermediate representation"); + ( "-smt", + set_target "smt", + " print SMT translated version of input"); ( "-c", Arg.Tuple [set_target "c"; Arg.Set Initial_check.opt_undefined_gen], " output a C translated version of the input"); @@ -408,6 +411,19 @@ let target name out_name ast type_envs = flush output_chan; if close then close_out output_chan else () + | Some "smt" -> + let ast_smt, type_envs = Specialize.(specialize typ_ord_specialization ast type_envs) in + (* let ast_smt, type_envs = Specialize.(specialize' 1 int_specialization_with_externs ast_smt type_envs) in *) + let close, output_chan = + match !opt_file_out with + | Some f -> Util.opt_colors := false; (true, open_out (f ^ ".smt2")) + | None -> false, stdout + in + Util.opt_warnings := true; + Jib_smt.generate_smt output_chan type_envs ast_smt; + flush output_chan; + if close then close_out output_chan else () + | Some "lem" -> output "" (Lem_out (!opt_libs_lem)) [(out_name, type_envs, ast)] |