From ab1eff9c6aa26e477fb9014c83022769ce3811a0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lb@leliobrun.net>
Date: Thu, 2 Mar 2023 18:33:50 +0900
Subject: [PATCH] fix a bug where some files were not generated if -acsl-spec
was not present
---
dune | 1 +
src/backends/C/c_backend.ml | 104 ++++++++++++++++++------------------
src/optimize_machine.ml | 16 +++---
3 files changed, 60 insertions(+), 61 deletions(-)
diff --git a/dune b/dune
index 188ccb8d..a6fdfd5b 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 3e25da04..79ac82c7 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 5e4accbc..4cfc7005 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
--
GitLab