sig
  module Analysis :
    sig
      val compute : unit -> unit
      val is_computed : unit -> bool
      val self : State.t
      type computation_state = NotComputed | Computing | Computed | Aborted
      val current_computation_state : unit -> Eva.Analysis.computation_state
      val register_computation_hook :
        ?on:Eva.Analysis.computation_state ->
        (Eva.Analysis.computation_state -> unit) -> unit
      type results = Complete | Partial | NoResults
      type status =
          Unreachable
        | SpecUsed
        | Builtin of string
        | Analyzed of Eva.Analysis.results
      val status : Cil_types.kernel_function -> Eva.Analysis.status
      val use_spec_instead_of_definition : Cil_types.kernel_function -> bool
      val save_results : Cil_types.kernel_function -> bool
    end
  module Results :
    sig
      val are_available : Cil_types.kernel_function -> bool
      type callstack = (Cil_types.kernel_function * Cil_types.kinstr) list
      type request
      type value
      type address
      type 'a evaluation
      type error = Bottom | Top | DisabledDomain
      type 'a result = ('a, Eva.Results.error) Result.t
      val string_of_error : Eva.Results.error -> string
      val pretty_error : Stdlib.Format.formatter -> Eva.Results.error -> unit
      val pretty_result :
        (Stdlib.Format.formatter -> '-> unit) ->
        Stdlib.Format.formatter -> 'Eva.Results.result -> unit
      val default : '-> 'Eva.Results.result -> 'a
      val at_start : Eva.Results.request
      val at_end : unit -> Eva.Results.request
      val at_start_of : Cil_types.kernel_function -> Eva.Results.request
      val at_end_of : Cil_types.kernel_function -> Eva.Results.request
      val before : Cil_types.stmt -> Eva.Results.request
      val after : Cil_types.stmt -> Eva.Results.request
      val before_kinstr : Cil_types.kinstr -> Eva.Results.request
      val in_callstack :
        Eva.Results.callstack -> Eva.Results.request -> Eva.Results.request
      val in_callstacks :
        Eva.Results.callstack list ->
        Eva.Results.request -> Eva.Results.request
      val filter_callstack :
        (Eva.Results.callstack -> bool) ->
        Eva.Results.request -> Eva.Results.request
      val callstacks : Eva.Results.request -> Eva.Results.callstack list
      val by_callstack :
        Eva.Results.request ->
        (Eva.Results.callstack * Eva.Results.request) list
      val equality_class :
        Cil_types.exp ->
        Eva.Results.request -> Cil_types.exp list Eva.Results.result
      val get_cvalue_model : Eva.Results.request -> Cvalue.Model.t
      val get_cvalue_model_result :
        Eva.Results.request -> Cvalue.Model.t Eva.Results.result
      val expr_deps :
        Cil_types.exp -> Eva.Results.request -> Locations.Zone.t
      val lval_deps :
        Cil_types.lval -> Eva.Results.request -> Locations.Zone.t
      val address_deps :
        Cil_types.lval -> Eva.Results.request -> Locations.Zone.t
      val eval_var :
        Cil_types.varinfo ->
        Eva.Results.request -> Eva.Results.value Eva.Results.evaluation
      val eval_lval :
        Cil_types.lval ->
        Eva.Results.request -> Eva.Results.value Eva.Results.evaluation
      val eval_exp :
        Cil_types.exp ->
        Eva.Results.request -> Eva.Results.value Eva.Results.evaluation
      val eval_address :
        ?for_writing:bool ->
        Cil_types.lval ->
        Eva.Results.request -> Eva.Results.address Eva.Results.evaluation
      val eval_callee :
        Cil_types.exp ->
        Eva.Results.request -> Kernel_function.t list Eva.Results.result
      val as_int :
        Eva.Results.value Eva.Results.evaluation -> int Eva.Results.result
      val as_integer :
        Eva.Results.value Eva.Results.evaluation ->
        Integer.t Eva.Results.result
      val as_float :
        Eva.Results.value Eva.Results.evaluation -> float Eva.Results.result
      val as_ival :
        Eva.Results.value Eva.Results.evaluation -> Ival.t Eva.Results.result
      val as_fval :
        Eva.Results.value Eva.Results.evaluation -> Fval.t Eva.Results.result
      val as_cvalue : Eva.Results.value Eva.Results.evaluation -> Cvalue.V.t
      val as_cvalue_result :
        Eva.Results.value Eva.Results.evaluation ->
        Cvalue.V.t Eva.Results.result
      val as_cvalue_or_uninitialized :
        Eva.Results.value Eva.Results.evaluation ->
        Cvalue.V_Or_Uninitialized.t
      val as_location :
        Eva.Results.address Eva.Results.evaluation ->
        Locations.location Eva.Results.result
      val as_zone :
        Eva.Results.address Eva.Results.evaluation -> Locations.Zone.t
      val as_zone_result :
        Eva.Results.address Eva.Results.evaluation ->
        Locations.Zone.t Eva.Results.result
      val is_singleton : 'Eva.Results.evaluation -> bool
      val is_initialized : Eva.Results.value Eva.Results.evaluation -> bool
      val alarms : 'Eva.Results.evaluation -> Alarms.t list
      val is_empty : Eva.Results.request -> bool
      val is_bottom : 'Eva.Results.evaluation -> bool
      val is_called : Cil_types.kernel_function -> bool
      val is_reachable : Cil_types.stmt -> bool
      val is_reachable_kinstr : Cil_types.kinstr -> bool
      val condition_truth_value : Cil_types.stmt -> bool * bool
      val callers :
        Cil_types.kernel_function -> Cil_types.kernel_function list
      val callsites :
        Cil_types.kernel_function ->
        (Cil_types.kernel_function * Cil_types.stmt list) list
      val callee : Cil_types.stmt -> Kernel_function.t list
    end
  module Parameters :
    sig
      val enabled_domains : unit -> (string * string) list
      val use_builtin : Cil_types.kernel_function -> string -> unit
      val use_global_value_partitioning : Cil_types.varinfo -> unit
    end
  module Eva_annotations :
    sig
      type slevel_annotation =
          SlevelMerge
        | SlevelDefault
        | SlevelLocal of int
        | SlevelFull
      type unroll_annotation = UnrollAmount of Cil_types.term | UnrollFull
      type split_kind = Static | Dynamic
      type split_term =
          Expression of Cil_types.exp
        | Predicate of Cil_types.predicate
      type flow_annotation =
          FlowSplit of Eva.Eva_annotations.split_term *
            Eva.Eva_annotations.split_kind
        | FlowMerge of Eva.Eva_annotations.split_term
      type allocation_kind = By_stack | Fresh | Fresh_weak | Imprecise
      type array_segmentation =
          Cil_types.varinfo * Cil_types.offset * Cil_types.exp list
      type domain_scope = string * Cil_types.varinfo list
      val get_slevel_annot :
        Cil_types.stmt -> Eva.Eva_annotations.slevel_annotation option
      val get_unroll_annot :
        Cil_types.stmt -> Eva.Eva_annotations.unroll_annotation list
      val get_flow_annot :
        Cil_types.stmt -> Eva.Eva_annotations.flow_annotation list
      val get_subdivision_annot : Cil_types.stmt -> int list
      val get_allocation :
        Cil_types.stmt -> Eva.Eva_annotations.allocation_kind
      val add_slevel_annot :
        emitter:Emitter.t ->
        Cil_types.stmt -> Eva.Eva_annotations.slevel_annotation -> unit
      val add_unroll_annot :
        emitter:Emitter.t ->
        Cil_types.stmt -> Eva.Eva_annotations.unroll_annotation -> unit
      val add_flow_annot :
        emitter:Emitter.t ->
        Cil_types.stmt -> Eva.Eva_annotations.flow_annotation -> unit
      val add_subdivision_annot :
        emitter:Emitter.t -> Cil_types.stmt -> int -> unit
      val add_array_segmentation :
        emitter:Emitter.t ->
        Cil_types.stmt -> Eva.Eva_annotations.array_segmentation -> unit
      val add_domain_scope :
        emitter:Emitter.t ->
        Cil_types.stmt -> Eva.Eva_annotations.domain_scope -> unit
    end
  module Eval : sig type cacheable = Cacheable | NoCache | NoCacheCallers end
  module Builtins :
    sig
      exception Invalid_nb_of_args of int
      exception Outside_builtin_possibilities
      type builtin_type = unit -> Cil_types.typ * Cil_types.typ list
      type cacheable =
        Eva.Eval.cacheable =
          Cacheable
        | NoCache
        | NoCacheCallers
      type full_result = {
        c_values : (Cvalue.V.t option * Cvalue.Model.t) list;
        c_clobbered : Base.SetLattice.t;
        c_from : (Function_Froms.froms * Locations.Zone.t) option;
      }
      type call_result =
          States of Cvalue.Model.t list
        | Result of Cvalue.V.t list
        | Full of Eva.Builtins.full_result
      type builtin =
          Cvalue.Model.t ->
          (Cil_types.exp * Cvalue.V.t) list -> Eva.Builtins.call_result
      val register_builtin :
        string ->
        ?replace:string ->
        ?typ:Eva.Builtins.builtin_type ->
        Eva.Builtins.cacheable -> Eva.Builtins.builtin -> unit
      val is_builtin : string -> bool
    end
  module Eval_terms :
    sig
      val annot_predicate_deps :
        pre:Cvalue.Model.t ->
        here:Cvalue.Model.t -> Cil_types.predicate -> Locations.Zone.t option
    end
  module Eva_results :
    sig
      type results
      val get_results : unit -> Eva.Eva_results.results
      val set_results : Eva.Eva_results.results -> unit
      val merge :
        Eva.Eva_results.results ->
        Eva.Eva_results.results -> Eva.Eva_results.results
      val change_callstacks :
        (Value_types.callstack -> Value_types.callstack) ->
        Eva.Eva_results.results -> Eva.Eva_results.results
    end
  module Unit_tests : sig val run : unit -> unit end
end