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