functor
  (Abstract : Abstractions.S) (Eva : sig
                                       type state = Abstract.Dom.t
                                       type value = Abstract.Val.t
                                       type origin = Abstract.Dom.origin
                                       type loc = Abstract.Loc.location
                                       module Valuation :
                                         sig
                                           type t
                                           type value = value
                                           type origin = origin
                                           type loc = loc
                                           val empty : t
                                           val find :
                                             t ->
                                             Cil_types.exp ->
                                             (value, origin) Eval.record_val
                                             Eval.or_top
                                           val add :
                                             t ->
                                             Cil_types.exp ->
                                             (value, origin) Eval.record_val ->
                                             t
                                           val fold :
                                             (Cil_types.exp ->
                                              (value, origin) Eval.record_val ->
                                              '-> 'a) ->
                                             t -> '-> 'a
                                           val find_loc :
                                             t ->
                                             Cil_types.lval ->
                                             loc Eval.record_loc Eval.or_top
                                           val remove :
                                             t -> Cil_types.exp -> t
                                           val remove_loc :
                                             t -> Cil_types.lval -> t
                                         end
                                       val evaluate :
                                         ?valuation:Valuation.t ->
                                         ?reduction:bool ->
                                         state ->
                                         Cil_types.exp ->
                                         (Valuation.t * value) Eval.evaluated
                                       val copy_lvalue :
                                         ?valuation:Valuation.t ->
                                         state ->
                                         Cil_types.lval ->
                                         (Valuation.t *
                                          value Eval.flagged_value)
                                         Eval.evaluated
                                       val lvaluate :
                                         ?valuation:Valuation.t ->
                                         for_writing:bool ->
                                         state ->
                                         Cil_types.lval ->
                                         (Valuation.t * loc * Cil_types.typ)
                                         Eval.evaluated
                                       val reduce :
                                         ?valuation:Valuation.t ->
                                         state ->
                                         Cil_types.exp ->
                                         bool -> Valuation.t Eval.evaluated
                                       val assume :
                                         ?valuation:Valuation.t ->
                                         state ->
                                         Cil_types.exp ->
                                         value -> Valuation.t Eval.or_bottom
                                       val split_by_evaluation :
                                         Cil_types.exp ->
                                         Integer.t list ->
                                         state list ->
                                         (Integer.t * state list * bool) list *
                                         state list
                                       val check_non_overlapping :
                                         state ->
                                         Cil_types.lval list ->
                                         Cil_types.lval list ->
                                         unit Eval.evaluated
                                       val eval_function_exp :
                                         Cil_types.exp ->
                                         ?args:Cil_types.exp list ->
                                         state ->
                                         (Kernel_function.t * Valuation.t)
                                         list Eval.evaluated
                                     end->
  sig
    val compute_from_entry_point :
      Cil_types.kernel_function -> lib_entry:bool -> unit
    val compute_from_init_state :
      Cil_types.kernel_function -> Abstract.Dom.t -> unit
    val initial_state : lib_entry:bool -> Abstract.Dom.t Eval.or_bottom
  end