From 7f9aabea50f78d3c3728c8bf2c2b3bcc45850c18 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lelio.brun@isae-supaero.fr>
Date: Tue, 10 May 2022 18:25:10 +0200
Subject: [PATCH] reorganize internal libraries to solve execution failures for
other executables than lustrec
---
src/backends/C/c_backend_makefile.ml | 4 +-
src/dune | 64 +++++++++++++++-------------
src/main_lustre_testgen.ml | 4 +-
src/options_management.ml | 4 +-
src/sites_paths.ml | 2 +
src/sites_paths.mli | 2 +
src/version.ml | 2 -
src/version.mli | 2 -
8 files changed, 45 insertions(+), 39 deletions(-)
create mode 100644 src/sites_paths.ml
create mode 100644 src/sites_paths.mli
diff --git a/src/backends/C/c_backend_makefile.ml b/src/backends/C/c_backend_makefile.ml
index 38f7c80a..0a7820f3 100644
--- a/src/backends/C/c_backend_makefile.ml
+++ b/src/backends/C/c_backend_makefile.ml
@@ -63,7 +63,7 @@ let pp_print_dependencies arrow_suffix fmt deps =
List.map
(fun dep ->
(if dep.local then dep.name
- else Version.include_path ^ "/" ^ dep.name)
+ else Sites_paths.include_path ^ "/" ^ dep.name)
^ ".c")
compiled_deps
in
@@ -136,7 +136,7 @@ functor
binname
Sys.executable_name
(Filename.dirname (Filename.dirname Sys.executable_name))
- Version.include_path
+ Sites_paths.include_path
(* Main binary *)
basename
"run"
diff --git a/src/dune b/src/dune
index bddbd951..39d94634 100644
--- a/src/dune
+++ b/src/dune
@@ -6,12 +6,11 @@
(include_subdirs unqualified)
(library
- (name lustrec_interface)
+ (name lustrec_core)
(package lustrec)
(modules_without_implementation scheduling_type machine_code_types)
(modules
lustre_types
- lustre_utils
utils
location
dimension
@@ -19,37 +18,21 @@
real
types
options
- version
clocks
delay
- scheduling_type
+ log
+ corelang
machine_code_types
spec_types
- spec_common
- lustre_live
- log
+ scheduling_type
printers
- corelang
basic_library
+ version
type_predef
+ annotations
clock_predef
- delay_predef
error
global
- annotations
- machine_code_common
- arrow
- options_management
- stateless
- c_backend_common
- typing
- ocaml_utils
- backends
- lustrec_mpfr
- normalization
- arrow_taint
- machine_types
- splitting
compiler_common
parse
parser_lustre
@@ -58,9 +41,34 @@
lexer_lustre
lexerLustreSpec
automata
- clock_calculus)
+ stateless
+ typing
+ clock_calculus
+ backends
+ normalization
+ machine_types
+ splitting)
+ (wrapped false)
+ (libraries ocamlgraph menhirLib zarith unix))
+
+(library
+ (name lustrec_interface)
+ (package lustrec)
+ (modules
+ lustre_utils
+ spec_common
+ lustre_live
+ delay_predef
+ machine_code_common
+ arrow
+ sites_paths
+ options_management
+ c_backend_common
+ ocaml_utils
+ lustrec_mpfr
+ arrow_taint)
(wrapped false)
- (libraries sites ocamlgraph zarith unix str menhirLib))
+ (libraries lustrec_core sites str))
(library
(name plugin_register)
@@ -71,7 +79,6 @@
(generate_sites_module
(module sites)
- ; (sites lustrec)
(plugins
(lustrec plugins)
(lustrec verifiers)))
@@ -126,7 +133,7 @@
c_backend_main
plugins)
(wrapped false)
- (libraries sites lustrec_interface plugin_register))
+ (libraries lustrec_interface plugin_register))
(executable
(name main_lustre_compiler)
@@ -139,13 +146,12 @@
(name main_lustre_testgen)
(public_name lustret)
(modules main_lustre_testgen mutation pathConditions)
- (libraries lustrec_lib))
+ (libraries lustrec_core lustrec_lib))
(library
(name verifier_register)
(package lustrec)
(wrapped false)
- ; (modules_without_implementation verifierType)
(modules verifierList verifierType)
(libraries lustrec_interface))
diff --git a/src/main_lustre_testgen.ml b/src/main_lustre_testgen.ml
index 8f15747c..8871b296 100644
--- a/src/main_lustre_testgen.ml
+++ b/src/main_lustre_testgen.ml
@@ -158,11 +158,11 @@ let testgen_source dirname basename extension =
Format.fprintf
cmake_fmt
"include(\"%s/helpful_functions.cmake\")@."
- Version.testgen_path;
+ Sites_paths.testgen_path;
Format.fprintf
cmake_fmt
"include(\"%s/FindLustre.cmake\")@."
- Version.testgen_path;
+ Sites_paths.testgen_path;
Format.fprintf cmake_fmt "LUSTREFILES(LFILES ${CMAKE_CURRENT_SOURCE_DIR} )@.";
Format.fprintf cmake_fmt "@[<v 2>FOREACH(lus_file ${LFILES})@ ";
Format.fprintf cmake_fmt "get_lustre_name_ext(${lus_file} L E)@ ";
diff --git a/src/options_management.ml b/src/options_management.ml
index c7f00109..80f2f691 100644
--- a/src/options_management.ml
+++ b/src/options_management.ml
@@ -20,7 +20,7 @@ let print_version () =
User provided include directory: @[<h>%a@]@]@."
Version.number
Version.codename
- Version.include_path
+ Sites_paths.include_path
(pp_print_list ~pp_sep:pp_print_space pp_print_string)
!include_dirs
@@ -38,7 +38,7 @@ let add_include_dir dir =
perform a fold_right to respect the order *)
let search_lib_path (local, full_file_name) =
let paths =
- if local then !include_dirs else Version.include_path :: !include_dirs
+ if local then !include_dirs else Sites_paths.include_path :: !include_dirs
in
let name =
List.fold_right
diff --git a/src/sites_paths.ml b/src/sites_paths.ml
new file mode 100644
index 00000000..ba37a848
--- /dev/null
+++ b/src/sites_paths.ml
@@ -0,0 +1,2 @@
+let include_path = Sites.Sites.include_ |> List.hd
+let testgen_path = Sites.Sites.testgen |> List.hd
diff --git a/src/sites_paths.mli b/src/sites_paths.mli
new file mode 100644
index 00000000..e66b8391
--- /dev/null
+++ b/src/sites_paths.mli
@@ -0,0 +1,2 @@
+val include_path : string
+val testgen_path : string
diff --git a/src/version.ml b/src/version.ml
index de05425e..90127837 100644
--- a/src/version.ml
+++ b/src/version.ml
@@ -1,4 +1,2 @@
let number = "@PACKAGE_VERSION@-@GITBRANCH@"
let codename = "@VERSION_CODENAME@"
-let include_path = Sites.Sites.include_ |> List.hd
-let testgen_path = Sites.Sites.testgen |> List.hd
diff --git a/src/version.mli b/src/version.mli
index 58fc63e4..e1f7bfcf 100644
--- a/src/version.mli
+++ b/src/version.mli
@@ -1,4 +1,2 @@
val number : string
val codename : string
-val include_path : string
-val testgen_path : string
--
GitLab