sig
  module Value_results :
    sig
      type results
      val get_results : unit -> Eva.Value_results.results
      val set_results : Eva.Value_results.results -> unit
      val merge :
        Eva.Value_results.results ->
        Eva.Value_results.results -> Eva.Value_results.results
      val change_callstacks :
        (Value_types.callstack -> Value_types.callstack) ->
        Eva.Value_results.results -> Eva.Value_results.results
    end
  module Value_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 Eval_terms :
    sig
      type eval_env
      type logic_deps = Locations.Zone.t Cil_datatype.Logic_label.Map.t
      type labels_states = Db.Value.state Cil_datatype.Logic_label.Map.t
      val env_annot :
        ?c_labels:Eva.Eval_terms.labels_states ->
        pre:Db.Value.state ->
        here:Db.Value.state -> unit -> Eva.Eval_terms.eval_env
      val predicate_deps :
        Eva.Eval_terms.eval_env ->
        Cil_types.predicate -> Eva.Eval_terms.logic_deps option
    end
  module Unit_tests : sig val run : unit -> 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 flow_annotation =
          FlowSplit of Cil_types.term
        | FlowMerge of Cil_types.term
      val add_slevel_annot :
        emitter:Emitter.t ->
        loc:Cil_types.location ->
        Cil_types.stmt -> Eva.Eva_annotations.slevel_annotation -> unit
      val add_unroll_annot :
        emitter:Emitter.t ->
        loc:Cil_types.location ->
        Cil_types.stmt -> Eva.Eva_annotations.unroll_annotation -> unit
      val add_flow_annot :
        emitter:Emitter.t ->
        loc:Cil_types.location ->
        Cil_types.stmt -> Eva.Eva_annotations.flow_annotation -> unit
      val add_subdivision_annot :
        emitter:Emitter.t ->
        loc:Cil_types.location -> Cil_types.stmt -> int -> unit
    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 = 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
end