sig
  module type Domain =
    sig
      type state
      type eval_env
      val env_current_state : eval_env -> state Eval.or_bottom
      val env_annot : pre:state -> here:state -> unit -> eval_env
      val env_pre_f : pre:state -> unit -> eval_env
      val env_post_f :
        pre:state ->
        post:state -> result:Cil_types.varinfo option -> unit -> eval_env
      val eval_predicate : eval_env -> Cil_types.predicate -> Alarmset.status
      val reduce_by_predicate :
        eval_env -> bool -> Cil_types.predicate -> eval_env
      type t = state
      val ty : t Type.t
      val name : string
      val descr : t Descr.t
      val packed_descr : Structural_descr.pack
      val reprs : t list
      val equal : t -> t -> bool
      val compare : t -> t -> int
      val hash : t -> int
      val pretty_code : Format.formatter -> t -> unit
      val internal_pretty_code :
        Type.precedence -> Format.formatter -> t -> unit
      val pretty : Format.formatter -> t -> unit
      val varname : t -> string
      val mem_project : (Project_skeleton.t -> bool) -> t -> bool
      val copy : t -> t
    end
  module ActiveBehaviors :
    sig
      type t
      val is_active :
        Transfer_logic.ActiveBehaviors.t ->
        Cil_types.behavior -> Alarmset.status
      val active_behaviors :
        Transfer_logic.ActiveBehaviors.t -> Cil_types.behavior list
      val behavior_from_name :
        Transfer_logic.ActiveBehaviors.t -> string -> Cil_types.behavior
    end
  val process_inactive_behaviors :
    Cil_types.kernel_function ->
    Cil_types.kinstr -> Transfer_logic.ActiveBehaviors.t -> unit
  val process_inactive_postconds :
    Cil_types.kernel_function -> Cil_types.behavior list -> unit
  module type S =
    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
  module Make :
    functor
      (Domain : Domain) (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 map_or_bottom :
                                      (state -> state Eval.or_bottom) ->
                                      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
        val create : state -> Cil_types.kernel_function -> ActiveBehaviors.t
        val create_from_spec : state -> Cil_types.spec -> ActiveBehaviors.t
        val check_fct_preconditions_for_behavior :
          Cil_types.kernel_function ->
          ActiveBehaviors.t ->
          per_behavior:bool ->
          Cil_types.kinstr -> states -> Cil_types.behavior -> states
        val check_fct_preconditions :
          Cil_types.kernel_function ->
          ActiveBehaviors.t ->
          Cil_types.kinstr -> state -> states Eval.or_bottom
        val check_fct_postconditions_for_behaviors :
          Cil_types.kernel_function ->
          ActiveBehaviors.t ->
          Cil_types.behavior list ->
          Cil_types.termination_kind ->
          per_behavior:bool ->
          pre_state:state ->
          post_states:states -> result:Cil_types.varinfo option -> states
        val check_fct_postconditions :
          Cil_types.kernel_function ->
          ActiveBehaviors.t ->
          Cil_types.termination_kind ->
          pre_state:state ->
          post_states:states ->
          result:Cil_types.varinfo option -> states Eval.or_bottom
        val reduce_by_assumes_of_behavior :
          Cil_types.kernel_function -> Cil_types.behavior -> states -> states
        val interp_annot :
          limit:int ->
          record:bool ->
          Cil_types.kernel_function ->
          ActiveBehaviors.t ->
          Cil_types.stmt ->
          Cil_types.code_annotation ->
          initial_state:state -> states -> states
      end
end