sig
type state
type value
type summary
val assign :
with_alarms:CilE.warn_mode ->
Transfer_stmt.S.state ->
Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.lval -> Cil_types.exp -> Transfer_stmt.S.state Eval.or_bottom
val assume :
with_alarms:CilE.warn_mode ->
Transfer_stmt.S.state ->
Cil_types.stmt ->
Cil_types.exp -> bool -> Transfer_stmt.S.state Eval.or_bottom
val call :
with_alarms:CilE.warn_mode ->
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 * Value_types.cacheable
val return :
with_alarms:CilE.warn_mode ->
Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.lval option ->
Transfer_stmt.S.state ->
(Transfer_stmt.S.state, Transfer_stmt.S.summary, Transfer_stmt.S.value)
Eval.return Eval.or_bottom
val split_final_states :
Cil_types.kernel_function ->
Cil_types.exp ->
Integer.t list ->
Transfer_stmt.S.state list -> Transfer_stmt.S.state list list
val check_unspecified_sequence :
with_alarms:CilE.warn_mode ->
Transfer_stmt.S.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 res =
(Transfer_stmt.S.state, Transfer_stmt.S.summary, Transfer_stmt.S.value)
Eval.call_result * Value_types.cacheable
val compute_call_ref :
(Cil_types.kinstr ->
Transfer_stmt.S.value Eval.call ->
Transfer_stmt.S.state -> Transfer_stmt.S.res)
Pervasives.ref
end