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