Module Equality_domain

module Equality_domain: sig .. end

Initial abstract state at the beginning of a call. From most precise to less precise.


type call_init_state = 
| ISCaller (*

information from the caller is propagated in the callee. May be more precise, but problematic w.r.t Memexec because it increases cache miss dramatically.

*)
| ISFormals (*

empty state, except for the equalities between a formal and the corresponding actual. Lesser impact on Memexec.

*)
| ISEmpty (*

completely empty state, without impact on Memexec.

*)
type t 
val key : t Abstract_domain.key
val project : t -> Equality.Set.t
module Make: 
functor (Value : Abstract.Value.External-> sig .. end