sig
  module Make :
    functor
      (Abstract : Abstractions.S) (States : sig
                                              type state = Abstract.Dom.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) (Logic : sig
                                                            type state =
                                                                Abstract.Dom.t
                                                            type states =
                                                                States.t
                                                            val create :
                                                              state ->
                                                              Cil_types.kernel_function ->
                                                              Transfer_logic.ActiveBehaviors.t
                                                            val create_from_spec :
                                                              state ->
                                                              Cil_types.spec ->
                                                              Transfer_logic.ActiveBehaviors.t
                                                            val check_fct_preconditions_for_behaviors :
                                                              Cil_types.kinstr ->
                                                              Cil_types.kernel_function ->
                                                              Cil_types.behavior
                                                              list ->
                                                              Alarmset.status ->
                                                              states ->
                                                              states
                                                            val check_fct_preconditions :
                                                              Cil_types.kinstr ->
                                                              Cil_types.kernel_function ->
                                                              Transfer_logic.ActiveBehaviors.t ->
                                                              state ->
                                                              states
                                                              Eval.or_bottom
                                                            val check_fct_postconditions_for_behaviors :
                                                              Cil_types.kernel_function ->
                                                              Cil_types.behavior
                                                              list ->
                                                              Alarmset.status ->
                                                              pre_state:
                                                              state ->
                                                              post_states:
                                                              states ->
                                                              result:
                                                              Cil_types.varinfo
                                                              option ->
                                                              states
                                                            val check_fct_postconditions :
                                                              Cil_types.kernel_function ->
                                                              Transfer_logic.ActiveBehaviors.t ->
                                                              Cil_types.termination_kind ->
                                                              pre_state:
                                                              state ->
                                                              post_states:
                                                              states ->
                                                              result:
                                                              Cil_types.varinfo
                                                              option ->
                                                              states
                                                              Eval.or_bottom
                                                            val evaluate_assumes_of_behavior :
                                                              state ->
                                                              Cil_types.behavior ->
                                                              Alarmset.status
                                                            val interp_annot :
                                                              limit:int ->
                                                              record:
                                                              bool ->
                                                              Cil_types.kernel_function ->
                                                              Transfer_logic.ActiveBehaviors.t ->
                                                              Cil_types.stmt ->
                                                              Cil_types.code_annotation ->
                                                              initial_state:
                                                              state ->
                                                              states ->
                                                              states
                                                          end->
      sig
        val treat_statement_assigns :
          Cil_types.assigns -> Abstract.Dom.t -> Abstract.Dom.t
        val compute_using_specification :
          warn:bool ->
          Cil_types.kinstr ->
          (Abstract.Loc.location, Abstract.Val.t) Eval.call ->
          Cil_types.spec ->
          Abstract.Dom.t -> Abstract.Dom.t list Eval.or_bottom
      end
end