diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli index fc8896e0d68517d862d8a0670e7605de21fff13f..1c07614bd1a1376f87fc6b08ca8d95b5495baf8f 100644 --- a/src/plugins/eva/Eva.mli +++ b/src/plugins/eva/Eva.mli @@ -68,6 +68,9 @@ module Analysis: sig finishes. If [on] is given, the hook will only be called when the analysis switches to this specific state. *) + val emitter: Emitter.t + (** Emitter used by Eva to emit property statuses. *) + (** Kind of results for the analysis of a function body. *) type results = | Complete diff --git a/src/plugins/eva/engine/analysis.ml b/src/plugins/eva/engine/analysis.ml index 2b63e58b9f02008b7c7a865bc8a44dc2e540140a..f1fc2d5ff1ed3d2b1f99acaf51d0e0815518134c 100644 --- a/src/plugins/eva/engine/analysis.ml +++ b/src/plugins/eva/engine/analysis.ml @@ -29,6 +29,7 @@ let current_computation_state = Self.current_computation_state let register_computation_hook = Self.register_computation_hook let is_computed = Self.is_computed let self = Self.state +let emitter = Eva_utils.emitter type results = Function_calls.results = Complete | Partial | NoResults type status = Function_calls.analysis_status = diff --git a/src/plugins/eva/engine/analysis.mli b/src/plugins/eva/engine/analysis.mli index cd472bcd27b2e9f8b29a4c1c8e763b1fcf10710b..be2d743c970b9b935bff2fb5bfa5b2f260628f01 100644 --- a/src/plugins/eva/engine/analysis.mli +++ b/src/plugins/eva/engine/analysis.mli @@ -108,6 +108,9 @@ val register_computation_hook: ?on:computation_state -> finishes. If [on] is given, the hook will only be called when the analysis switches to this specific state. *) +val emitter: Emitter.t +(** Emitter used by Eva to emit property statuses. *) + (** Kind of results for the analysis of a function body. *) type results = | Complete