[e-acsl] first review

src/plugins/e-acsl/src/analyses/analyses_datatype.ml

@@ -395,14 +395,15 @@ 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"
-    in {env with let_quantif_bind = new_lq_bind}
+        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}
 
 end
 

src/plugins/e-acsl/src/analyses/analyses_datatype.mli

@@ -76,20 +76,28 @@ module LFProf: Datatype.S_with_collections
     - an association list for variables bound by a let or a quantification *)
 module Logic_env : sig
   type t
-  (* forward reference to meet of intervals *)
+
+  (** forward reference to meet of intervals *)
   val ival_meet_ref : (ival -> ival -> ival) ref
-  (* add a new binding for a let or a quantification binder only *)
+
+  (** add a new binding for a let or a quantification binder only *)
   val add : t -> logic_var -> ival -> t
-  (* the empty environment *)
+
+  (** the empty environment *)
   val empty : t
-  (* create a new environment from a profile, for function calls *)
+
+  (** create a new environment from a profile, for function calls *)
   val make : Profile.t -> t
-  (* find a logic variable in the environment *)
+
+  (** find a logic variable in the environment *)
   val find : t -> logic_var -> ival
-  (* get the profile of the logic environment, i.e. bindings through function
+
+  (** get the profile of the logic environment, i.e. bindings through function
      arguments *)
   val get_profile : t -> Profile.t
-  (* refine the interval of a logic variable *)
+
+  (** 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

@@ -687,7 +687,8 @@ let rec infer ~force ~logic_env t =
     | Tif (t1, t2, t3) ->
       ignore (infer ~force ~logic_env t1);
       let logic_env_tbranch, logic_env_fbranch =
-        compute_logic_env_if_branches logic_env t1 in
+        compute_logic_env_if_branches logic_env t1
+      in
       let i2 = infer ~force ~logic_env:logic_env_tbranch t2 in
       let i3 = infer ~force ~logic_env:logic_env_fbranch t3 in
       Error.map2 join i2 i3
@@ -878,7 +879,6 @@ and infer_term_host ~force ~logic_env thost =
         Printer.pp_typ ty
         Printer.pp_term t
 
-
 and infer_term_offset ~force ~logic_env t =
   match t with
   | TNoOffset -> ()
@@ -888,18 +888,20 @@ and infer_term_offset ~force ~logic_env t =
     ignore (infer ~force ~logic_env t);
     infer_term_offset ~force ~logic_env toff
 
+(* Update the interval of variables when they appear in a comparison of the form
+   [x op t] or [t op x] *)
 and compute_logic_env_if_branches logic_env t =
   let get_res = Error.map (fun x -> x) in
   let ival v = infer ~force:false ~logic_env v in
   let add_ub logic_env x v =
     let max = Ival.max_int (Error.map extract_ival (ival v)) in
     Logic_env.refine logic_env x (Ival (Ival.inject_range None max))
-  and add_lb logic_env x v =
+  in
+  let add_lb logic_env x v =
     let min = Ival.min_int (Error.map extract_ival (ival v)) in
     Logic_env.refine logic_env x (Ival (Ival.inject_range min None))
-  and add_eq logic_env x v =
-    Logic_env.refine logic_env x (get_res (ival v))
   in
+  let add_eq logic_env x v = Logic_env.refine logic_env x (get_res (ival v)) in
   let t_branch, f_branch =
     match t.term_node with
     | TBinOp(op, {term_node = TLval(TVar x, TNoOffset)}, v) ->