sig
  type state
  type states
  val create :
    Transfer_logic.S.state -> Cil_types.kernel_function -> Active_behaviors.t
  val create_from_spec :
    Transfer_logic.S.state -> Cil_types.spec -> Active_behaviors.t
  val check_fct_preconditions_for_behaviors :
    Cil_types.kinstr ->
    Cil_types.kernel_function ->
    Cil_types.behavior list ->
    Alarmset.status -> Transfer_logic.S.states -> Transfer_logic.S.states
  val check_fct_preconditions :
    Cil_types.kinstr ->
    Cil_types.kernel_function ->
    Active_behaviors.t ->
    Transfer_logic.S.state -> Transfer_logic.S.states Eval.or_bottom
  val check_fct_postconditions_for_behaviors :
    Cil_types.kernel_function ->
    Cil_types.behavior list ->
    Alarmset.status ->
    pre_state:Transfer_logic.S.state ->
    post_states:Transfer_logic.S.states ->
    result:Cil_types.varinfo option -> Transfer_logic.S.states
  val check_fct_postconditions :
    Cil_types.kernel_function ->
    Active_behaviors.t ->
    Cil_types.termination_kind ->
    pre_state:Transfer_logic.S.state ->
    post_states:Transfer_logic.S.states ->
    result:Cil_types.varinfo option -> Transfer_logic.S.states Eval.or_bottom
  val evaluate_assumes_of_behavior :
    Transfer_logic.S.state -> Cil_types.behavior -> Alarmset.status
  val interp_annot :
    limit:int ->
    record:bool ->
    Cil_types.kernel_function ->
    Active_behaviors.t ->
    Cil_types.stmt ->
    Cil_types.code_annotation ->
    initial_state:Transfer_logic.S.state ->
    Transfer_logic.S.states -> Transfer_logic.S.states
end