From e1c716faf54ed2b637ca5684cfcd45ab1f2b9ddc 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:58:00 +0100
Subject: [PATCH] [Eva] Abstract domains: removes type context from Transfer.
It is only used in Queries.
---
src/plugins/eva/domains/abstract_domain.ml | 2 --
src/plugins/eva/domains/cvalue/cvalue_transfer.ml | 1 -
src/plugins/eva/domains/taint_domain.ml | 3 +--
3 files changed, 1 insertion(+), 5 deletions(-)
diff --git a/src/plugins/eva/domains/abstract_domain.ml b/src/plugins/eva/domains/abstract_domain.ml
index 64bc8ec4fd8..465a10b220e 100644
--- a/src/plugins/eva/domains/abstract_domain.ml
+++ b/src/plugins/eva/domains/abstract_domain.ml
@@ -222,7 +222,6 @@ type ('value, 'location, 'origin) valuation =
(** Transfer function of the domain. *)
module type Transfer = sig
type state
- type context
type value
type location
type origin
@@ -403,7 +402,6 @@ module type S = sig
(** Transfer functions from the result of evaluations.
See {!Eval} for more details about valuation. *)
include Transfer with type state := t
- and type context := context
and type value := value
and type location := location
and type origin := origin
diff --git a/src/plugins/eva/domains/cvalue/cvalue_transfer.ml b/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
index 97fa2c84c83..42610cca8f0 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
@@ -23,7 +23,6 @@
open Cil_types
open Eval
-type context = unit
type value = Main_values.CVal.t
type origin = value
type location = Main_locations.PLoc.location
diff --git a/src/plugins/eva/domains/taint_domain.ml b/src/plugins/eva/domains/taint_domain.ml
index af2aa971e15..e0b0d4f3c07 100644
--- a/src/plugins/eva/domains/taint_domain.ml
+++ b/src/plugins/eva/domains/taint_domain.ml
@@ -315,8 +315,7 @@ module Domain = struct
include QueriesTaint
include (TransferTaint: Abstract_domain.Transfer
- with type context := context
- and type state := state
+ with type state := state
and type value := value
and type location := location
and type origin := origin)
--
GitLab