diff --git a/src/plugins/value/utils/results.ml b/src/plugins/value/utils/results.ml index c74ee12715f98008731072f2caadac3f3dce0193..2ee26e12af1a65e9114e38b771fe2b7e6fa0c3d0 100644 --- a/src/plugins/value/utils/results.ml +++ b/src/plugins/value/utils/results.ml @@ -254,8 +254,29 @@ struct let callstacks req = Response.callstacks (get_by_callstack req) - let equality_class _exp _req = - raise Not_implemented (* Where is the key for Equality_domain ? *) + let equality_class exp req = + let open Equality in + match A.Dom.get Equality_domain.key with + | None -> + Result.error DisabledDomain + | Some extract -> + let hce = Hcexprs.HCE.of_exp exp in + let extract' state = + let equalities = Equality_domain.project (extract state) in + NonTrivial (Set.find hce equalities) + and reduce e1 e2 = + match e1, e2 with + | Trivial, _ | _, Trivial -> Trivial + | NonTrivial e1, NonTrivial e2 -> Equality.inter e1 e2 + in + let r = match Response.map_join extract' reduce (get req) with + | (`Top | `Bottom) as r -> r + | `Value Trivial -> `Top + | `Value (NonTrivial e) -> + let l = Equality.elements e in + `Value (List.map Hcexprs.HCE.to_exp l) + in + convert r let as_cvalue_model req = match A.Dom.get Cvalue_domain.State.key with diff --git a/src/plugins/value/utils/results.mli b/src/plugins/value/utils/results.mli index b70dd4a4bcc295e136b255c8925c09ac7057226d..50b1505f08d3355cce2a281462e3ec0348c588af 100644 --- a/src/plugins/value/utils/results.mli +++ b/src/plugins/value/utils/results.mli @@ -57,7 +57,7 @@ val filter_callstack : (callstack -> bool) -> request -> request (* State requests *) val callstacks : request -> callstack list -val equality_class : Cil_types.exp -> request -> Cil_types.exp list option +val equality_class : Cil_types.exp -> request -> Cil_types.exp list result val as_cvalue_model : request -> Cvalue.Model.t result (* Evaluation *)