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