sig
  val save_results : Cil_types.fundec -> bool
  val partial_results : unit -> bool
  type analysis_target =
      [ `Builtin of
          string * Builtins.builtin * Eval.cacheable * Cil_types.funspec
      | `Def of Cil_types.fundec * bool
      | `Spec of Cil_types.funspec ]
  val define_analysis_target :
    ?recursion_depth:int ->
    Cil_types.kinstr ->
    Cil_types.kernel_function -> Function_calls.analysis_target
  val use_spec_instead_of_definition :
    ?recursion_depth:int -> Cil_types.kernel_function -> bool
  val is_called : Cil_types.kernel_function -> 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
  type results = Complete | Partial | NoResults
  type analysis_status =
      Unreachable
    | SpecUsed
    | Builtin of string
    | Analyzed of Function_calls.results
  val analysis_status :
    Cil_types.kernel_function -> Function_calls.analysis_status
  type t
  val get_results : unit -> Function_calls.t
  val set_results : Function_calls.t -> unit
  val merge_results :
    Function_calls.t -> Function_calls.t -> Function_calls.t
end