sig
  module Make :
    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
end