From 5273a5b678c041f830f6d217eae752dc1beb0dea Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 13 Jul 2022 14:55:26 +0200
Subject: [PATCH] [Eva] New module Private, used internally but not exported in
Eva.mli.
The Eva gui and optional domains (numerors and apron) are compiled separately
from the Eva core. The Private module is used to give them access to the
internal Eva modules they need.
---
.gitattributes | 2 -
src/plugins/eva/{Eva.mli.in => Eva.header} | 33 ------------
src/plugins/eva/dune | 8 +--
src/plugins/eva/gen-api.sh | 8 +--
.../eva/{Eva.ml.in => utils/private.ml} | 49 +++++++++---------
src/plugins/eva/utils/private.mli | 50 +++++++++++++++++++
6 files changed, 82 insertions(+), 68 deletions(-)
rename src/plugins/eva/{Eva.mli.in => Eva.header} (63%)
rename src/plugins/eva/{Eva.ml.in => utils/private.ml} (64%)
create mode 100644 src/plugins/eva/utils/private.mli
diff --git a/.gitattributes b/.gitattributes
index cb4033a47d6..83ba44bdc1a 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 ee97ccf3957..61ed1ae7e5e 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 ee310c427be..cc13a58ece9 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 dea87c497c5..48b34c37516 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 9931040bf9c..c5a16ae1195 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 00000000000..d4c64ac5ad0
--- /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
--
GitLab