From 734e2c6957f5a9cd86dc518961288880fb9d11d4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 5 Mar 2024 15:53:04 +0100
Subject: [PATCH] [Eva] Uses name Context instead of Ctx in the equality
domain.
---
.../eva/domains/equality/equality_domain.ml | 9 +++++----
.../eva/domains/equality/equality_domain.mli | 14 +++++---------
2 files changed, 10 insertions(+), 13 deletions(-)
diff --git a/src/plugins/eva/domains/equality/equality_domain.ml b/src/plugins/eva/domains/equality/equality_domain.ml
index 2269e22db0a..67d3a38cdca 100644
--- a/src/plugins/eva/domains/equality/equality_domain.ml
+++ b/src/plugins/eva/domains/equality/equality_domain.ml
@@ -127,7 +127,7 @@ module Internal = struct
let pretty fmt (eqs, _, _) = Equality.Set.pretty fmt eqs
- let pretty_debug fmt (eqs, deps, modified) =
+ let _pretty_debug fmt (eqs, deps, modified) =
Format.fprintf fmt
"@[<v>@[<hov 2>Eqs: %a@]@.@[<hov 2>Deps: %a@]@.@[<hov 2>Changed: %a@]@]"
Equality.Set.pretty eqs Deps.pretty deps
@@ -179,19 +179,20 @@ let project (t, _, _) = t
module type Context = Abstract.Context.External
module type Value = Abstract.Value.External
-module Make (Ctx : Context) (Value : Value with type context = Ctx.t) = struct
+module Make (Context : Context) (Value : Value with type context = Context.t) =
+struct
include Internal
include Store
let get_cvalue = Value.get Main_values.CVal.key
- type context = Ctx.t
+ type context = Context.t
type value = Value.t
type location = Precise_locs.precise_location
type origin
- let return_context _ = `Value Ctx.top
+ let return_context _ = `Value Context.top
let reduce_further (equalities, _, _) expr value =
let atom = HCE.of_exp expr in
diff --git a/src/plugins/eva/domains/equality/equality_domain.mli b/src/plugins/eva/domains/equality/equality_domain.mli
index 729e7191ffe..aa35a9e3326 100644
--- a/src/plugins/eva/domains/equality/equality_domain.mli
+++ b/src/plugins/eva/domains/equality/equality_domain.mli
@@ -38,14 +38,10 @@ val project: t -> Equality.Set.t
module type Context = Abstract.Context.External
module type Value = Abstract.Value.External
-module Make (Ctx : Context) (Value : Value with type context = Ctx.t) : sig
- include Abstract_domain.S
- with type context = Ctx.t
- and type value = Value.t
- and type location = Precise_locs.precise_location
- and type state = t
-
- val pretty_debug : Format.formatter -> t -> unit
-end
+module Make (Context : Context) (Value : Value with type context = Context.t) :
+ Abstract_domain.S with type context = Context.t
+ and type value = Value.t
+ and type location = Precise_locs.precise_location
+ and type state = t
val registered : Abstractions.Domain.registered
--
GitLab