diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
index 473ce5547af126a357533a79d850e3fe18e452d3..a3cf92e62ec73bb4492fea68e8855d206df065f2 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
+++ b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
@@ -364,6 +364,11 @@ module Logic_env
type t = { profile : Profile.t;
let_quantif_bind : Profile.t}
+ (* forward reference to meet of intervals *)
+ let ival_meet_ref
+ : (ival -> ival -> ival) ref
+ = ref (fun _i1 _i2 -> Extlib.mk_labeled_fun "ival_meet_ref")
+
let add env x i =
{ env with let_quantif_bind = Logic_var.Map.add x i env.let_quantif_bind}
@@ -382,6 +387,23 @@ module Logic_env
let get_profile env = env.profile
+ let refine env x ival =
+ let update = function
+ | None -> raise Not_found
+ | Some i -> Some (!ival_meet_ref i ival)
+ in
+ 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}
+
end
(* Imperative environment to perform fixpoint algorithm for recursive
diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.mli b/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
index 008856976aa48dc11e4b8ac6c5459ca3c8e5870d..7a60fddb59c86789e208e261e074301819e13226 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
+++ b/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
@@ -76,6 +76,8 @@ 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 *)
+ val ival_meet_ref : (ival -> ival -> ival) ref
(* add a new binding for a let or a quantification binder only *)
val add : t -> logic_var -> ival -> t
(* the empty environment *)
@@ -87,6 +89,8 @@ module Logic_env : sig
(* 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 *)
+ 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 f68cae7dcf7b99d17e06792c8fc7208ba865af0c..3c2a82a928256462b81da59cb075c4475bd78d51 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -216,6 +216,8 @@ let meet i1 i2 = match i1, i2 with
| Nan, (Ival _ | Float _ | Rational | Real) ->
Nan
+let () = Logic_env.ival_meet_ref := meet
+
let is_singleton_int = function
| Ival iv -> Ival.is_singleton_int iv
| Float _ | Rational | Real | Nan -> false
@@ -372,7 +374,8 @@ let rec fixpoint ~(infer : force:bool ->
then
ival
else
- fixpoint ~infer li args_ival t' inferred_ival
+ let assumed_ival = interv_of_typ_containing_interv inferred_ival in
+ fixpoint ~infer li args_ival t' assumed_ival
(* Memoization module which retrieves the computed info of some terms *)
@@ -683,8 +686,10 @@ let rec infer ~force ~logic_env t =
Error.map (fun src -> cast ~src ~dst) src
| Tif (t1, t2, t3) ->
ignore (infer ~force ~logic_env t1);
- let i2 = infer ~force ~logic_env t2 in
- let i3 = infer ~force ~logic_env t3 in
+ let logic_env_tbranch, logic_env_fbranch =
+ 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
| Tat (t, _) ->
get_res (infer ~force ~logic_env t)
@@ -883,6 +888,59 @@ and infer_term_offset ~force ~logic_env t =
ignore (infer ~force ~logic_env t);
infer_term_offset ~force ~logic_env toff
+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 =
+ 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 t_branch, f_branch =
+ match t.term_node with
+ | TBinOp(op, {term_node = TLval(TVar x, TNoOffset)}, v) ->
+ begin
+ match op with
+ | Lt | Le ->
+ add_ub logic_env x v,
+ add_lb logic_env x v
+ | Gt | Ge ->
+ add_lb logic_env x v,
+ add_ub logic_env x v
+ | Eq ->
+ add_eq logic_env x v,
+ logic_env
+ | Ne ->
+ logic_env,
+ add_eq logic_env x v
+ | _ -> logic_env, logic_env
+ end
+ | _ -> logic_env, logic_env
+ in
+ match t.term_node with
+ | TBinOp(op, u, {term_node = TLval(TVar y, TNoOffset)}) ->
+ begin
+ match op with
+ | Lt | Le ->
+ add_lb t_branch y u,
+ add_ub f_branch y u
+ | Gt | Ge ->
+ add_ub t_branch y u,
+ add_lb f_branch y u
+ | Eq ->
+ add_eq t_branch y u,
+ logic_env
+ | Ne ->
+ logic_env,
+ add_eq f_branch y u
+ | _ -> t_branch, f_branch
+ end
+ | _ -> t_branch, f_branch
+
(* [type_bound_variables] infers an interval associated with each of
the provided bounds of a quantified variable, and provides a term
accordingly. It could happen that the bounds provided for a quantifier