diff --git a/.gitattributes b/.gitattributes
index cb4033a47d63786ebe95ba10a95ddfc906dd7738..83ba44bdc1a3908c2791fdcd9ea8a2082b1ff013 100644
--- a/.gitattributes
+++ b/.gitattributes
@@ -91,9 +91,7 @@ Make* header_spec=CEA_LGPL
*.js header_spec=CEA_LGPL
*.ml header_spec=CEA_LGPL
-*.ml.in header_spec=CEA_LGPL
*.mli header_spec=CEA_LGPL
-*.mli.in header_spec=CEA_LGPL
*.mll header_spec=CEA_LGPL
*.mly header_spec=CEA_LGPL
diff --git a/src/plugins/eva/Eva.mli.in b/src/plugins/eva/Eva.header
similarity index 63%
rename from src/plugins/eva/Eva.mli.in
rename to src/plugins/eva/Eva.header
index ee97ccf3957db006495ed5f04f863e94bfd56989..61ed1ae7e5e7fd4e7e9f70a98d8d2752ff3b2009 100644
--- a/src/plugins/eva/Eva.mli.in
+++ b/src/plugins/eva/Eva.header
@@ -19,36 +19,3 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
-
-(** ../.. *)
-
-(** For internal use *)
-(* Private first so that we do not override internal modules with public ones *)
-
-module Private: sig
- module Abstractions = Abstractions
- module Analysis = Analysis
- module Alarmset = Alarmset
- module Parameters = Parameters
- module Main_values = Main_values
- module Eval = Eval
- module Eva_utils = Eva_utils
- module Eva_results = Eva_results
- module Self = Self
- module Eval_terms = Eval_terms
- module Red_statuses = Red_statuses
- module Abstract_value = Abstract_value
- module Abstract_domain = Abstract_domain
- module Active_behaviors = Active_behaviors
- module Function_calls = Function_calls
- module Simple_memory = Simple_memory
- module Structure = Structure
- module Eval_typ = Eval_typ
- module Eval_op = Eval_op
- module Domain_builder = Domain_builder
- module Main_locations = Main_locations
- module Eval_annots = Eval_annots
- module Eva_dynamic = Eva_dynamic
-end
-
-(** ../.. *)
diff --git a/src/plugins/eva/dune b/src/plugins/eva/dune
index ee310c427bee2e7a3aa46ef91a121370bfa0714f..cc13a58ece9a0a3b8f5471e80b24fac98311052c 100644
--- a/src/plugins/eva/dune
+++ b/src/plugins/eva/dune
@@ -53,7 +53,7 @@
(name eva_gui)
(public_name frama-c-eva.gui)
(optional)
- (flags -open Frama_c_kernel -open Frama_c_gui -open Eva -open Eva.Private :standard -w -9)
+ (flags -open Frama_c_kernel -open Frama_c_gui -open Eva__Private :standard -w -9)
(libraries eva frama-c.kernel frama-c.gui)
))
@@ -64,7 +64,7 @@
(name numerors)
(optional)
(public_name frama-c-eva.numerors.core)
- (flags -open Frama_c_kernel -open Eva.Private :standard)
+ (flags -open Frama_c_kernel -open Eva__Private :standard)
(libraries frama-c.kernel frama-c-eva.core mlmpfr)
))
@@ -74,7 +74,7 @@
(subdir domains/apron ( library
(name apron_domain)
(public_name frama-c-eva.apron)
- (flags -open Frama_c_kernel -open Eva.Private :standard -w -9)
+ (flags -open Frama_c_kernel -open Eva__Private :standard -w -9)
(modules apron_domain)
(libraries frama-c.kernel frama-c-eva.core apron.octMPQ apron.boxMPQ apron.polkaMPQ apron.apron)
(optional)
@@ -86,7 +86,7 @@
(rule
(targets Eva.ml Eva.mli)
(deps
- gen-api.sh Eva.ml.in Eva.mli.in
+ gen-api.sh Eva.header
engine/analysis.mli utils/results.mli parameters.mli utils/eva_annotations.mli eval.mli
domains/cvalue/builtins.mli utils/cvalue_callbacks.mli legacy/eval_terms.mli utils/eva_results.mli utils/unit_tests.mli
)
diff --git a/src/plugins/eva/gen-api.sh b/src/plugins/eva/gen-api.sh
index dea87c497c5aa1b3f4abde3ced38687892beedb8..48b34c37516fd2f8e40fda698dfbaf34ddb5bbec 100755
--- a/src/plugins/eva/gen-api.sh
+++ b/src/plugins/eva/gen-api.sh
@@ -27,7 +27,7 @@ dir=$(dirname $0)
# Generate MLI
-cat $dir/Eva.mli.in >> Eva.mli
+cat $dir/Eva.header >> Eva.mli
printf '\n(** Eva public API.
@@ -48,7 +48,7 @@ printf '\n(* This file is generated. Do not edit. *)\n' >> Eva.mli
for i in "$@"
do
- if [[ ! "$i" =~ [.]in$ ]]; then
+ if [[ ! "$i" =~ [.]header$ ]]; then
file=$(basename $i)
module=${file%.*}
Module="$(echo "${module:0:1}" | tr '[:lower:]' '[:upper:]')${module:1}"
@@ -60,11 +60,11 @@ done
# Generate ML
-cat $dir/Eva.ml.in >> Eva.ml
+cat $dir/Eva.header >> Eva.ml
for i in "$@"
do
- if [[ ! "$i" =~ [.]in$ ]]; then
+ if [[ ! "$i" =~ [.]header$ ]]; then
file=$(basename $i)
module=${file%.*}
Module="$(echo "${module:0:1}" | tr '[:lower:]' '[:upper:]')${module:1}"
diff --git a/src/plugins/eva/Eva.ml.in b/src/plugins/eva/utils/private.ml
similarity index 64%
rename from src/plugins/eva/Eva.ml.in
rename to src/plugins/eva/utils/private.ml
index 9931040bf9c5e1673271d57bac9d1f99a26c09d9..c5a16ae11951cb4fec6bec7762131939b13ab083 100644
--- a/src/plugins/eva/Eva.ml.in
+++ b/src/plugins/eva/utils/private.ml
@@ -20,28 +20,27 @@
(* *)
(**************************************************************************)
-module Private = struct
- module Abstractions = Eva__Abstractions
- module Analysis = Eva__Analysis
- module Alarmset = Eva__Alarmset
- module Parameters = Parameters
- module Main_values = Eva__Main_values
- module Eval = Eva__Eval
- module Eval_terms = Eva__Eval_terms
- module Eva_utils = Eva_utils
- module Eva_results = Eva_results
- module Self = Self
- module Red_statuses = Eva__Red_statuses
- module Abstract_value = Eva__Abstract_value
- module Abstract_domain = Eva__Abstract_domain
- module Active_behaviors = Active_behaviors
- module Function_calls = Function_calls
- module Simple_memory = Eva__Simple_memory
- module Structure = Eva__Structure
- module Eval_typ = Eva__Eval_typ
- module Eval_op = Eva__Eval_op
- module Domain_builder = Eva__Domain_builder
- module Main_locations = Eva__Main_locations
- module Eval_annots = Eva__Eval_annots
- module Eva_dynamic = Eva_dynamic
-end
+module Abstract_domain = Abstract_domain
+module Abstract_value = Abstract_value
+module Abstractions = Abstractions
+module Active_behaviors = Active_behaviors
+module Alarmset = Alarmset
+module Analysis = Analysis
+module Domain_builder = Domain_builder
+module Eva_dynamic = Eva_dynamic
+module Eva_results = Eva_results
+module Eva_utils = Eva_utils
+module Eval = Eval
+module Eval_annots = Eval_annots
+module Eval_op = Eval_op
+module Eval_terms = Eval_terms
+module Eval_typ = Eval_typ
+module Function_calls = Function_calls
+module Main_locations = Main_locations
+module Main_values = Main_values
+module Parameters = Parameters
+module Red_statuses = Red_statuses
+module Results = Results
+module Self = Self
+module Simple_memory = Simple_memory
+module Structure = Structure
diff --git a/src/plugins/eva/utils/private.mli b/src/plugins/eva/utils/private.mli
new file mode 100644
index 0000000000000000000000000000000000000000..d4c64ac5ad0f0992d3ca624cae53a5b64421d9df
--- /dev/null
+++ b/src/plugins/eva/utils/private.mli
@@ -0,0 +1,50 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** For internal use only: the Eva gui and optional domains (numerors and apron)
+ are compiled separately from the Eva core. This is used to give them access
+ to the internal modules of Eva they need. *)
+
+module Abstract_domain = Abstract_domain
+module Abstract_value = Abstract_value
+module Abstractions = Abstractions
+module Active_behaviors = Active_behaviors
+module Alarmset = Alarmset
+module Analysis = Analysis
+module Domain_builder = Domain_builder
+module Eva_dynamic = Eva_dynamic
+module Eva_results = Eva_results
+module Eva_utils = Eva_utils
+module Eval = Eval
+module Eval_annots = Eval_annots
+module Eval_op = Eval_op
+module Eval_terms = Eval_terms
+module Eval_typ = Eval_typ
+module Function_calls = Function_calls
+module Main_locations = Main_locations
+module Main_values = Main_values
+module Parameters = Parameters
+module Red_statuses = Red_statuses
+module Results = Results
+module Self = Self
+module Simple_memory = Simple_memory
+module Structure = Structure