functor (Abstract : Abstractions.Eva) ->
sig
type state = Abstract.Dom.t
type value = Abstract.Val.t
type loc = Abstract.Loc.location
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 -> (Partition.key * state) list * Eval.cacheable
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 ref list)
list -> unit Eval.or_bottom
val enter_scope :
Cil_types.kernel_function -> Cil_types.varinfo list -> state -> state
type call_result = {
states : (Partition.key * state) list;
cacheable : Eval.cacheable;
builtin : bool;
}
val compute_call_ref :
(Cil_types.stmt ->
(loc, value) Eval.call ->
Eval.recursion option -> state -> call_result)
ref
end