fix a bug where some files were not generated if -acsl-spec was not present

dune

@@ -40,4 +40,5 @@
  (files share/FindLustre.cmake share/helpful_functions.cmake))
 
 ; ignore lustrec_wp_strategies directory
+
 (data_only_dirs lustrec_wp_strategies)

src/backends/C/c_backend.ml

@@ -47,59 +47,59 @@ let gen_files generate_spec_header
   let destname = !Options.dest_dir ^ "/" ^ basename in
 
   (* Generating H spec file *)
-  if generate_spec_header then (
-    let spec_header_file = destname ^ "_spec.h" in
-    with_out_file spec_header_file (fun header_fmt ->
-        print_spec_header header_fmt basename machines dependencies);
-
-    (* Generating H memory file *)
-    let memory_header_file = destname ^ "_memory.h" in
-    with_out_file memory_header_file (fun header_fmt ->
-        print_memory_header header_fmt basename machines dependencies);
-
-    (* Generating H alloc file *)
-    let alloc_header_file = destname ^ "_alloc.h" in
+  (if generate_spec_header then
+   let spec_header_file = destname ^ "_spec.h" in
+   with_out_file spec_header_file (fun header_fmt ->
+       print_spec_header header_fmt basename machines dependencies));
+
+  (* Generating H memory file *)
+  let memory_header_file = destname ^ "_memory.h" in
+  with_out_file memory_header_file (fun header_fmt ->
+      print_memory_header header_fmt basename machines dependencies);
+
+  (* Generating H alloc file *)
+  let alloc_header_file = destname ^ "_alloc.h" in
+  (* Could be changed *)
+  with_out_file alloc_header_file (fun header_fmt ->
+      print_alloc_header header_fmt basename machines dependencies);
+
+  (* Generating Lib C file *)
+  let source_lib_file = c_or_cpp destname in
+  with_out_file source_lib_file (fun source_lib_fmt ->
+      print_lib_c source_lib_fmt basename prog machines dependencies);
+
+  (* Generating Main C file *)
+  let main_node = !Options.main_node in
+  with_main_node machines main_node (fun m ->
+      let source_main_file = c_or_cpp (destname ^ "_main") in
+      with_out_file source_main_file (fun source_main_fmt ->
+          print_main_c source_main_fmt m basename prog machines dependencies));
+
+  (* Generating Mauve files *)
+  with_main_node machines !Options.mauve (fun m ->
+      let source_mauve_file = destname ^ "_mauve.hpp" in
+      with_out_file source_mauve_file (fun source_mauve_fmt ->
+          (* Header *)
+          print_mauve_header source_mauve_fmt basename;
+          (* Shell *)
+          print_mauve_shell source_mauve_fmt m;
+          (* Core *)
+          print_mauve_core source_mauve_fmt m;
+          (* FSM *)
+          print_mauve_fsm source_mauve_fmt m));
+
+  (* Generating Makefile *)
+  (* Makefiles: - for the moment two cases 1. Classical Makefile, only when
+     provided with a main node May contain additional framac eacsl targets 2.
+     Cmake : 2 files - lustrec-basename.cmake describing all variables - the
+     main CMakeLists.txt activating the first file - Later option 1 should be
+     removed *)
+  (* Case 1 *)
+  if main_node <> "" then
+    let makefile_file = destname ^ ".makefile" in
     (* Could be changed *)
-    with_out_file alloc_header_file (fun header_fmt ->
-        print_alloc_header header_fmt basename machines dependencies);
-
-    (* Generating Lib C file *)
-    let source_lib_file = c_or_cpp destname in
-    with_out_file source_lib_file (fun source_lib_fmt ->
-        print_lib_c source_lib_fmt basename prog machines dependencies);
-
-    (* Generating Main C file *)
-    let main_node = !Options.main_node in
-    with_main_node machines main_node (fun m ->
-        let source_main_file = c_or_cpp (destname ^ "_main") in
-        with_out_file source_main_file (fun source_main_fmt ->
-            print_main_c source_main_fmt m basename prog machines dependencies));
-
-    (* Generating Mauve files *)
-    with_main_node machines !Options.mauve (fun m ->
-        let source_mauve_file = destname ^ "_mauve.hpp" in
-        with_out_file source_mauve_file (fun source_mauve_fmt ->
-            (* Header *)
-            print_mauve_header source_mauve_fmt basename;
-            (* Shell *)
-            print_mauve_shell source_mauve_fmt m;
-            (* Core *)
-            print_mauve_core source_mauve_fmt m;
-            (* FSM *)
-            print_mauve_fsm source_mauve_fmt m));
-
-    (* Generating Makefile *)
-    (* Makefiles: - for the moment two cases 1. Classical Makefile, only when
-       provided with a main node May contain additional framac eacsl targets 2.
-       Cmake : 2 files - lustrec-basename.cmake describing all variables - the
-       main CMakeLists.txt activating the first file - Later option 1 should be
-       removed *)
-    (* Case 1 *)
-    if main_node <> "" then
-      let makefile_file = destname ^ ".makefile" in
-      (* Could be changed *)
-      with_out_file makefile_file (fun makefile_fmt ->
-          print_makefile basename main_node dependencies makefile_fmt))
+    with_out_file makefile_file (fun makefile_fmt ->
+        print_makefile basename main_node dependencies makefile_fmt)
 
 (* (\* Case 2 *\) *)
 (* let cmake_file = "lustrec-" ^ basename ^ ".cmake" in *)

src/optimize_machine.ml

@@ -786,13 +786,12 @@ and instrs_are_skip instrs = List.for_all instr_is_skip instrs
 
 let instr_cons instr cont =
   match instr_is_skip instr, cont with
-  | true, [] -> [ { instr with instr_desc = MComment "" } ]
-  | true, i :: cont -> { i with instr_spec = i.instr_spec @ instr.instr_spec } :: cont
-  | false, _ -> instr :: cont
-  (* let instr_desc = *)
-  (*   if instr_is_skip instr then MComment "" else instr.instr_desc in *)
-  (* let instr = { instr with instr_desc } in *)
-  (* instr :: cont *)
+  | true, [] ->
+    [ { instr with instr_desc = MComment "" } ]
+  | true, i :: cont ->
+    { i with instr_spec = i.instr_spec @ instr.instr_spec } :: cont
+  | false, _ ->
+    instr :: cont
 
 (* XXX: UNUSED *)
 (* let rec instr_remove_skip instr cont =
@@ -1474,8 +1473,7 @@ let optimize params prog node_schs machine_code =
       let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in
       machine_code
       |> machines_reuse_variables reuse_tables
-      |> machines_fusion
-      |> machines_clean
+      |> machines_fusion |> machines_clean
     else machine_code
   in