diff --git a/dune b/dune index 188ccb8dfef3c72da62c8c6d04cad5b36a6ff34c..a6fdfd5b7354bda265b39ac56b485ba0c1bfd8c2 100644 --- a/dune +++ b/dune @@ -40,4 +40,5 @@ (files share/FindLustre.cmake share/helpful_functions.cmake)) ; ignore lustrec_wp_strategies directory + (data_only_dirs lustrec_wp_strategies) diff --git a/src/backends/C/c_backend.ml b/src/backends/C/c_backend.ml index 3e25da04d2d01c386b496ce1fdb6f05c3898a90f..79ac82c76e25dee82f543e8b042399b8f2325b74 100644 --- a/src/backends/C/c_backend.ml +++ b/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 *) diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml index 5e4accbc90ff336a41721522b27d010120245af9..4cfc7005961b4bb03b78c0b49129a31e2618b492 100644 --- a/src/optimize_machine.ml +++ b/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