functor
  (Abstract : Abstractions.Eva) (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) (Transfer : sig
                                                             type state =
                                                                 Abstract.Dom.t
                                                             type value =
                                                                 Abstract.Val.t
                                                             type location
                                                             val assign :
                                                               state ->
                                                               Cil_types.kinstr ->
                                                               Cil_types.lval ->
                                                               Cil_types.exp ->
                                                               state
                                                               Eval.or_bottom
                                                             val assume :
                                                               state ->
                                                               Cil_types.stmt ->
                                                               Cil_types.exp ->
                                                               bool ->
                                                               state
                                                               Eval.or_bottom
                                                             val call :
                                                               Cil_types.stmt ->
                                                               Cil_types.lval
                                                               option ->
                                                               Cil_types.exp ->
                                                               Cil_types.exp
                                                               list ->
                                                               state ->
                                                               state list
                                                               Eval.or_bottom *
                                                               Value_types.cacheable
                                                             val check_unspecified_sequence :
                                                               Cil_types.stmt ->
                                                               state ->
                                                               (Cil_types.stmt *
                                                                Cil_types.lval
                                                                list *
                                                                Cil_types.lval
                                                                list *
                                                                Cil_types.lval
                                                                list *
                                                                Cil_types.stmt
                                                                ref list)
                                                               list ->
                                                               unit
                                                               Eval.or_bottom
                                                             val enter_scope :
                                                               Cil_types.kernel_function ->
                                                               Cil_types.varinfo
                                                               list ->
                                                               state -> state
                                                             type call_result = {
                                                               states :
                                                                 state list
                                                                 Eval.or_bottom;
                                                               cacheable :
                                                                 Value_types.cacheable;
                                                               builtin : bool;
                                                             }
                                                             val compute_call_ref :
                                                               (Cil_types.stmt ->
                                                                (location,
                                                                 value)
                                                                Eval.call ->
                                                                state ->
                                                                call_result)
                                                               ref
                                                           end) (Init : 
  sig
    val initial_state :
      lib_entry:bool -> Abstract.Dom.t Bottom.Type.or_bottom
    val initial_state_with_formals :
      lib_entry:bool ->
      Cil_types.kernel_function -> Abstract.Dom.t Bottom.Type.or_bottom
    val initialize_local_variable :
      Cil_types.stmt ->
      Cil_types.varinfo ->
      Cil_types.init ->
      Abstract.Dom.t -> Abstract.Dom.t Bottom.Type.or_bottom
  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) (Spec : sig
                               val treat_statement_assigns :
                                 Cil_types.assigns ->
                                 Abstract.Dom.t -> Abstract.Dom.t
                             end->
  sig
    val compute :
      Cil_types.kernel_function ->
      Cil_types.kinstr ->
      Abstract.Dom.t ->
      Abstract.Dom.t list Eval.or_bottom * Value_types.cacheable
  end