sig
type state
type value
type loc
val assign :
Transfer_stmt.S.state ->
Cil_types.kinstr ->
Cil_types.lval -> Cil_types.exp -> Transfer_stmt.S.state Eval.or_bottom
val assume :
Transfer_stmt.S.state ->
Cil_types.stmt ->
Cil_types.exp -> bool -> Transfer_stmt.S.state Eval.or_bottom
val call :
Cil_types.stmt ->
Cil_types.lval option ->
Cil_types.exp ->
Cil_types.exp list ->
Transfer_stmt.S.state ->
Transfer_stmt.S.state list Eval.or_bottom * Eval.cacheable
val check_unspecified_sequence :
Cil_types.stmt ->
Transfer_stmt.S.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 -> Transfer_stmt.S.state -> Transfer_stmt.S.state
type call_result = {
states : Transfer_stmt.S.state list Eval.or_bottom;
cacheable : Eval.cacheable;
builtin : bool;
}
val compute_call_ref :
(Cil_types.stmt ->
(Transfer_stmt.S.loc, Transfer_stmt.S.value) Eval.call ->
Eval.recursion option ->
Transfer_stmt.S.state -> Transfer_stmt.S.call_result)
Stdlib.ref
end