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. | *) |
module Make: