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
    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
end