sig
  type state
  type value
  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 * Value_types.cacheable
  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 :
    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 Pervasives.ref list)
    list -> unit Eval.or_bottom
  type call_result = {
    states : Transfer_stmt.S.state list Eval.or_bottom;
    cacheable : Value_types.cacheable;
  }
  val compute_call_ref :
    (Cil_types.kinstr ->
     Transfer_stmt.S.value Eval.call ->
     Transfer_stmt.S.state -> Transfer_stmt.S.call_result)
    Pervasives.ref
end