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 loc
                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 -> (Partition.key * state) list * Eval.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 : (Partition.key * state) list;
                  cacheable : Eval.cacheable;
                  builtin : bool;
                }
                val compute_call_ref :
                  (Cil_types.stmt ->
                   (loc, value) Eval.call ->
                   Eval.recursion option -> state -> call_result)
                  ref
              end)
  (Init : sig
            val initial_state :
              lib_entry:bool -> Abstract.Dom.t Lattice_bounds.or_bottom
            val initial_state_with_formals :
              lib_entry:bool ->
              Cil_types.kernel_function ->
              Abstract.Dom.t Lattice_bounds.or_bottom
            val initialize_local_variable :
              Cil_types.stmt ->
              Cil_types.varinfo ->
              Cil_types.init ->
              Abstract.Dom.t -> Abstract.Dom.t Lattice_bounds.or_bottom
          end)
  (Logic : sig
             type state = Abstract.Dom.t
             type states = States.t
             val create :
               state -> Cil_types.kernel_function -> Active_behaviors.t
             val create_from_spec :
               state -> Cil_types.spec -> Active_behaviors.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 ->
               Active_behaviors.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 ->
               Active_behaviors.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 ->
               Active_behaviors.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 :
      save_results:bool ->
      Cil_types.kernel_function ->
      Cil_types.kinstr ->
      Abstract.Dom.t ->
      (Partition.key * Abstract.Dom.t) list * Eval.cacheable
  end