sig
  module type S =
    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
  module Make :
    functor
      (Domain : Abstract_domain.S) (States : sig
                                               type state = Domain.t
                                               type t
                                               val empty : t
                                               val is_empty : t -> bool
                                               val singleton : state -> t
                                               val singleton' :
                                                 state Eval.or_bottom -> t
                                               val uncheck_add :
                                                 state -> t -> t
                                               val add : state -> t -> t
                                               val add' :
                                                 state Eval.or_bottom ->
                                                 t -> t
                                               val length : t -> int
                                               val merge :
                                                 into:t -> t -> t * bool
                                               val join :
                                                 ?into:state Eval.or_bottom ->
                                                 t -> state Eval.or_bottom
                                               val fold :
                                                 (state -> '-> 'a) ->
                                                 t -> '-> 'a
                                               val iter :
                                                 (state -> unit) -> t -> unit
                                               val map :
                                                 (state -> state) -> t -> t
                                               val reorder : t -> t
                                               val of_list : state list -> t
                                               val to_list : t -> state list
                                               val pretty :
                                                 Format.formatter ->
                                                 t -> unit
                                             end->
      sig
        type state = Domain.t
        type states = States.t
        type active_behaviors
        val create : state -> Cil_types.kernel_function -> active_behaviors
        val check_fct_preconditions :
          Cil_types.kernel_function ->
          active_behaviors ->
          Cil_types.kinstr -> state -> states Eval.or_bottom
        val check_fct_postconditions :
          Cil_types.kernel_function ->
          active_behaviors ->
          Cil_types.termination_kind ->
          init_state:state ->
          post_states:states ->
          result:Cil_types.varinfo option -> states Eval.or_bottom
        val interp_annot :
          limit:int ->
          record:bool ->
          Cil_types.kernel_function ->
          active_behaviors ->
          Cil_types.stmt ->
          Cil_types.code_annotation ->
          initial_state:state -> states -> states
      end
end