sig
  type state
  type states
  val create :
    Transfer_logic.S.state ->
    Cil_types.kernel_function -> Transfer_logic.ActiveBehaviors.t
  val create_from_spec :
    Transfer_logic.S.state ->
    Cil_types.spec -> Transfer_logic.ActiveBehaviors.t
  val check_fct_preconditions_for_behavior :
    Cil_types.kernel_function ->
    Transfer_logic.ActiveBehaviors.t ->
    per_behavior:bool ->
    Cil_types.kinstr ->
    Transfer_logic.S.states -> Cil_types.behavior -> Transfer_logic.S.states
  val check_fct_preconditions :
    Cil_types.kernel_function ->
    Transfer_logic.ActiveBehaviors.t ->
    Cil_types.kinstr ->
    Transfer_logic.S.state -> Transfer_logic.S.states Eval.or_bottom
  val check_fct_postconditions_for_behaviors :
    Cil_types.kernel_function ->
    Transfer_logic.ActiveBehaviors.t ->
    Cil_types.behavior list ->
    Cil_types.termination_kind ->
    per_behavior:bool ->
    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 ->
    Transfer_logic.ActiveBehaviors.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 reduce_by_assumes_of_behavior :
    Cil_types.kernel_function ->
    Cil_types.behavior -> Transfer_logic.S.states -> Transfer_logic.S.states
  val interp_annot :
    limit:int ->
    record:bool ->
    Cil_types.kernel_function ->
    Transfer_logic.ActiveBehaviors.t ->
    Cil_types.stmt ->
    Cil_types.code_annotation ->
    initial_state:Transfer_logic.S.state ->
    Transfer_logic.S.states -> Transfer_logic.S.states
end