Functor Transfer_stmt.Make

module Make: 
functor (Value : Abstract_value.External) ->
functor (Location : Abstract_location.External) ->
functor (Domain : Abstract_domain.External with type value = Value.t and type location = Location.location) ->
functor (Eva : Evaluation.S with type state = Domain.state and type value = Domain.value and type loc = Domain.location and type origin = Domain.origin) -> S with type state = Domain.state and type value = Domain.value
Parameters:
Value : Abstract_value.External
Location : Abstract_location.External
Domain : Abstract_domain.External with type value = Value.t and type location = Location.location
Eva : Evaluation.S with type state = Domain.state and type value = Domain.value and type loc = Domain.location and type origin = Domain.origin

type state 
type value 
val assign : state ->
Cil_types.kinstr ->
Cil_types.lval -> Cil_types.exp -> state Eval.or_bottom
val assume : state ->
Cil_types.stmt ->
Cil_types.exp -> bool -> state Eval.or_bottom
val call : Cil_types.stmt ->
Cil_types.lval option ->
Cil_types.exp ->
Cil_types.exp list ->
state ->
state list Eval.or_bottom * Value_types.cacheable
val split_final_states : Cil_types.kernel_function ->
Cil_types.exp ->
Integer.t list ->
state list -> state list list
val check_unspecified_sequence : Cil_types.stmt ->
state ->
(Cil_types.stmt * Cil_types.lval list * Cil_types.lval list *
Cil_types.lval list * Cil_types.stmt Pervasives.ref list)
list -> unit Eval.or_bottom
type call_result = {
   states : state list Eval.or_bottom;
   cacheable : Value_types.cacheable;
}
val compute_call_ref : (Cil_types.kinstr ->
value Eval.call ->
state -> call_result)
Pervasives.ref