From 6fa9731347feb8d8c423f0238d4725479eda84d1 Mon Sep 17 00:00:00 2001 From: Thibaut Benjamin <thibaut.benjamin@gmail.com> Date: Tue, 9 Aug 2022 10:53:47 +0200 Subject: [PATCH] [e-acsl] second review --- .../e-acsl/src/analyses/analyses_datatype.mli | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.mli b/src/plugins/e-acsl/src/analyses/analyses_datatype.mli index 894e45b91d8..a68b6880da6 100644 --- a/src/plugins/e-acsl/src/analyses/analyses_datatype.mli +++ b/src/plugins/e-acsl/src/analyses/analyses_datatype.mli @@ -105,18 +105,23 @@ end (** Imperative environment to perform the fixpoint algorithm for recursive functions *) module LF_env : sig - (* find the currently infered interval for a call to a logic function *) + (** find the currently inferred interval for a call to a logic function *) val find : logic_info -> Profile.t -> ival - (* clear the table of intervals for logic function (to do between typing ) - each logic function calls *) + + (** clear the table of intervals for logic function (to do between typing ) + each logic function calls *) val clear : unit -> unit - (* add an interval for a logic function call *) + + (** add an interval as the current one for a logic function call *) val add : logic_info -> Profile.t -> ival -> unit - (* add an interval for a predicate call *) + + (** add 0..1 as the current interval for a predicate call *) val add_pred : logic_info -> Profile.t -> unit - (* determine wether a logic function or predicate is recursive *) + + (** determine whether a logic function or predicate is recursive *) val is_rec : logic_info -> bool - (* replace the current interval for a logic function call *) + + (** replace the current interval for a logic function call *) val replace : logic_info -> Profile.t -> ival -> unit end -- GitLab