sig
  type state
  type states
  type active_behaviors
  val create :
    Transfer_logic.S.state ->
    Cil_types.kernel_function -> Transfer_logic.S.active_behaviors
  val check_fct_preconditions :
    Cil_types.kernel_function ->
    Transfer_logic.S.active_behaviors ->
    Cil_types.kinstr ->
    Transfer_logic.S.state -> Transfer_logic.S.states Eval.or_bottom
  val check_fct_postconditions :
    Cil_types.kernel_function ->
    Transfer_logic.S.active_behaviors ->
    Cil_types.termination_kind ->
    init_state:Transfer_logic.S.state ->
    post_states:Transfer_logic.S.states ->
    result:Cil_types.varinfo option -> Transfer_logic.S.states Eval.or_bottom
  val interp_annot :
    limit:int ->
    record:bool ->
    Cil_types.kernel_function ->
    Transfer_logic.S.active_behaviors ->
    Cil_types.stmt ->
    Cil_types.code_annotation ->
    initial_state:Transfer_logic.S.state ->
    Transfer_logic.S.states -> Transfer_logic.S.states
end