From 384f3c5bcb5cdba85085f229e839601a59f11ed0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Tue, 19 Jul 2022 11:28:21 +0200 Subject: [PATCH] [Eva] Exports the Eva emitter in the Eva.mli API. --- src/plugins/eva/Eva.mli | 3 +++ src/plugins/eva/engine/analysis.ml | 1 + src/plugins/eva/engine/analysis.mli | 3 +++ 3 files changed, 7 insertions(+) diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli index fc8896e0d68..1c07614bd1a 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 2b63e58b9f0..f1fc2d5ff1e 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 cd472bcd27b..be2d743c970 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 -- GitLab