diff --git a/src/plugins/eva/domains/abstract_domain.ml b/src/plugins/eva/domains/abstract_domain.ml index 64bc8ec4fd8cbfda4347e51be7fe7ef96040d7b0..465a10b220e7bb84f0d28757dc7abb4f5e3b5081 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 97fa2c84c83f12a860b10d740c5d27e6043d6e2c..42610cca8f0c3d439baaf7b1a4f20af457c42593 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 af2aa971e151cc84512f77c90d4e8889200862ff..e0b0d4f3c07f1fd585db4313514983790a8ea1d4 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)