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