From 1f04474dc4f1cb58afc61a7c2c0f9d191dfed26f Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@gmail.com>
Date: Tue, 19 Jul 2022 11:18:40 +0200
Subject: [PATCH] [e-acsl] second review
---
.../e-acsl/src/analyses/analyses_datatype.ml | 14 +++++++-------
.../e-acsl/src/analyses/analyses_datatype.mli | 6 +++---
src/plugins/e-acsl/src/analyses/interval.ml | 4 ++++
3 files changed, 14 insertions(+), 10 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
index eaf5abc2297..ff6fc08f5e8 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
+++ b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
@@ -395,13 +395,13 @@ module Logic_env
let new_lq_bind =
try Logic_var.Map.update x update env.let_quantif_bind
with Not_found ->
- match Logic_var.Map.find_opt x env.profile with
- | Some i ->
- (* The profile must remain unchanged, so if the variable is bound in
- the profile, we add the refined interval in the other bindings,
- which are checked first when finding the interval *)
- Logic_var.Map.add x (!ival_meet_ref i ival) env.let_quantif_bind
- | None -> Options.abort "updating a variable not in environment"
+ match Logic_var.Map.find_opt x env.profile with
+ | Some i ->
+ (* The profile must remain unchanged, so if the variable is bound in
+ the profile, we add the refined interval in the other bindings,
+ which are checked first when finding the interval *)
+ Logic_var.Map.add x (!ival_meet_ref i ival) env.let_quantif_bind
+ | None -> Options.abort "updating a variable not in environment"
in
{env with let_quantif_bind = new_lq_bind}
diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.mli b/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
index 9aa1e9e288f..9cafe69c93a 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
+++ b/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
@@ -93,11 +93,11 @@ module Logic_env : sig
val find : t -> logic_var -> ival
(** get the profile of the logic environment, i.e. bindings through function
- arguments *)
+ arguments *)
val get_profile : t -> Profile.t
- (** refine the interval of a logic variable : replace an interval with a
- more precise one *)
+ (** refine the interval of a logic variable: replace an interval with a more
+ precise one *)
val refine : t -> logic_var -> ival -> t
end
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index c4810803071..833d84ed21d 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -903,6 +903,10 @@ and compute_logic_env_if_branches logic_env t =
in
let add_eq logic_env x v = Logic_env.refine logic_env x (get_res (ival v)) in
let t_branch, f_branch =
+ (* we do not discriminate between strict and weak inequalities. This is
+ slighlty less precise but allow for better reusing of the code in the
+ case of recursive functions, the main advantage in typing
+ conditionals is for recursive functions. *)
match t.term_node with
| TBinOp(op, {term_node = TLval(TVar x, TNoOffset)}, v) ->
begin
--
GitLab