Output folder for seal-extract

src/compiler_stages.ml

@@ -195,8 +195,9 @@ let stage1 params prog dirname basename extension =
   
   (* Compatibility with Lusi *)
   (* If compiling a lusi, generate the lusic. If this is a lus file, Check the existence of a lusi (Lustre Interface file) *)
-  compile_source_to_header
-    prog !Global.type_env !Global.clock_env dirname basename extension;
+  if !Options.compile_header then
+    compile_source_to_header
+      prog !Global.type_env !Global.clock_env dirname basename extension;
 
 
   let prog =

src/main_lustre_verifier.ml

@@ -43,7 +43,7 @@ we have multiple "backends"
 *)
 let rec verify dirname basename extension =
   let source_name = dirname ^ "/" ^ basename ^ extension in
-
+  Options.compile_header := false; (* to avoid producing .h / .lusic *)
   Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 0>");
   decr Options.verbose_level;
 

src/options.ml

@@ -34,6 +34,7 @@ let const_unfold = ref false
 let mpfr = ref false
 let mpfr_prec = ref 100
 let print_dec_types = ref false
+let compile_header = ref true
 
 (* Option to select the expected behavior of integer division: Euclidian or
    C. Default C !!! *)

src/tools/seal/seal_verifier.ml

@@ -34,7 +34,7 @@ let active = ref false
            
 (* Select the appropriate node, should have been inlined already and
    extract update/output functions. *)
-let seal_run basename prog machines =
+let seal_run ~basename prog machines =
   let node_name =
     match !Options.main_node with
     | "" -> (
@@ -99,7 +99,8 @@ let seal_run basename prog machines =
     );
   let new_node = Seal_export.to_lustre m sw_init sw_sys init_out update_out in  
   Format.eprintf "%a@." Printers.pp_node new_node;
-  let output_file = basename ^ "_seal.lus" in
+  let output_file = !Options.dest_dir ^ "/" ^ basename ^ "_seal.lus" in
+  Format.eprintf "%s@." output_file;
   let new_top = Corelang.mktop_decl Location.dummy_loc output_file false (Node new_node) in
 
   let out = open_out output_file in

src/tools/zustre/zustre_verifier.ml

@@ -158,7 +158,7 @@ module Verifier =
 
       Z3.Fixedpoint.set_parameters !fp fp_params
       
-    let run basename prog machines =
+    let run ~basename prog machines =
       let machines = Machine_code_common.arrow_machine::machines in
       let machines = preprocess machines in
       setup_solver ();

src/verifierType.ml

@@ -5,7 +5,7 @@ sig
   val is_active: unit -> bool
   val options: (string * Arg.spec * string) list
   val get_normalization_params: unit -> Normalization.param_t
-  val run: string -> Lustre_types.program_t -> Machine_code_types.machine_t list -> unit 
+  val run: basename:string -> Lustre_types.program_t -> Machine_code_types.machine_t list -> unit 
 end
 
 module Default =