module Make: functor (
Abstract
:
Abstractions.Eva
) ->
S
with type state = Abstract.Dom.t
and type value = Abstract.Val.t
and type loc = Abstract.Loc.location
type
state
type
value
type
loc
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 * 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 Stdlib.ref list)
list -> unit Eval.or_bottom
val enter_scope : Cil_types.kernel_function ->
Cil_types.varinfo list -> state -> state
type
call_result = {
}
val compute_call_ref : (Cil_types.stmt ->
(loc, value) Eval.call ->
Eval.recursion option ->
state -> call_result)
Stdlib.ref