Merge ast2C_proposition branch with the master one

src/ast_to_c.ml

@@ -310,12 +310,12 @@ let dump_var_locations fmt (st: node_states) =
 
 
 (** main function that prints a C-code from a term of type [t_nodelist]. *)
-let ast_to_c verbose debug prog =
+let ast_to_c fmt verbose debug prog =
   verbose "Computation of the node_states";
   let prog_st_types = make_state_types prog in
   debug (Format.asprintf "%a" dump_var_locations prog_st_types);
   let iprog: i_nodelist = ast_to_intermediate_ast prog prog_st_types in
-  Format.printf "%a\n\n%a\n\n%a\n\n/* Nodes: */\n%a%a\n"
+  Format.fprintf fmt "%a\n\n%a\n\n%a\n\n/* Nodes: */\n%a%a\n"
     cp_includes (Config.c_includes)
     cp_state_types prog_st_types
     cp_state_frees (iprog, prog_st_types)

src/main.ml

@@ -157,6 +157,13 @@ let _ =
     else (
       if !nopopt
         then (fun _ -> ())
-        else Ast_to_c.ast_to_c print_verbose print_debug)
+        else
+        (
+            let oc = open_out !output_file in
+            let fmt = Format.make_formatter
+                  (Stdlib.output_substring oc)
+                  (fun () -> Stdlib.flush oc) in
+            Ast_to_c.ast_to_c fmt print_verbose print_debug);
+        )
   end