From 76fcf7f929eaef185b92c291016b6440488f0fdd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 13 Mar 2024 10:39:15 +0100
Subject: [PATCH] [Eva] Abstractions.ml: minor change.
---
src/plugins/eva/engine/abstractions.ml | 6 +++---
src/plugins/eva/engine/abstractions.mli | 6 +++---
2 files changed, 6 insertions(+), 6 deletions(-)
diff --git a/src/plugins/eva/engine/abstractions.ml b/src/plugins/eva/engine/abstractions.ml
index 35bf38ebc70..a2dd68cb5b0 100644
--- a/src/plugins/eva/engine/abstractions.ml
+++ b/src/plugins/eva/engine/abstractions.ml
@@ -765,18 +765,18 @@ module Domain = struct
let build domains =
(* Build the contexts *)
- let interactive_ctx c = Context.(make_interactive c |> assert_not_unit) in
let contexts = List.fold_left add_contexts Context.init domains in
+ let interactive_ctx c = Context.(make_interactive c |> assert_not_unit) in
let module Contexts = (val interactive_ctx contexts) in
(* Build the values *)
let init_values = Value.init (module Contexts) in
- let interactive_value v = Value.(make_interactive v |> assert_not_unit) in
let values = List.fold_left add_values init_values domains in
+ let interactive_value v = Value.(make_interactive v |> assert_not_unit) in
let module Values = (val interactive_value values) in
(* Build the locations *)
let init_locations = Location.init (module Values) in
- let interactive_loc l = Location.(make_interactive l |> assert_not_unit) in
let locations = List.fold_left add_locations init_locations domains in
+ let interactive_loc l = Location.(make_interactive l |> assert_not_unit) in
let module Locs = (val interactive_loc locations) in
(* Build the domains *)
let init_domain = init (module Contexts) (module Values) (module Locs) in
diff --git a/src/plugins/eva/engine/abstractions.mli b/src/plugins/eva/engine/abstractions.mli
index a953bd11e81..482ba656537 100644
--- a/src/plugins/eva/engine/abstractions.mli
+++ b/src/plugins/eva/engine/abstractions.mli
@@ -24,9 +24,6 @@
module Domain : sig
- module type Context = Abstract.Context.External
- module type Value = Abstract.Value.External
-
(** Witness of the registration of an abstract domain, it can be used to
programmatically enable the domain. *)
type registered
@@ -52,6 +49,9 @@ module Domain : sig
name:string -> descr:string -> ?experimental:bool -> ?priority:int ->
(unit -> (module Abstract_domain.Leaf)) -> unit
+ module type Context = Abstract.Context.External
+ module type Value = Abstract.Value.External
+
(** Functor domain which can be built over any value abstractions, but with
fixed locations dependencies. *)
module type Functor = sig
--
GitLab