[e-acsl] second review

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}
 

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
 

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