diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
index ff6fc08f5e8d05749968825aaf6463db4c5df880..b8bbaba9d265107e15c83e773c664ffa7a4cba63 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
+++ b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
@@ -420,6 +420,9 @@ module LF_env
let add li profile ival = LFProf.Hashtbl.add tbl (li,profile) ival
+ let add_pred li profile = LFProf.Hashtbl.add tbl (li,profile)
+ (Ival Ival.zero_or_one)
+
exception Recursive
let contain li = object
diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.mli b/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
index 9cafe69c93a70301e49ffe2d73ccf84a3d6120c4..302d05c2656634b1096d1a4aa2b47c4e9011123b 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
+++ b/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
@@ -111,6 +111,8 @@ module LF_env : sig
val add : logic_info -> Profile.t -> ival -> unit
+ val add_pred : logic_info -> Profile.t -> unit
+
val is_rec : logic_info -> bool
val replace : logic_info -> Profile.t -> ival -> unit
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index 833d84ed21d5755e1b3763d8da9ac37b62d9d232..f2937821bc68e16241c86164a9964f1a9e12c215 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -739,28 +739,36 @@ let rec infer ~force ~logic_env t =
(fun arg -> get_res (infer ~force ~logic_env arg))
args)
in
- (match li.l_body with
- | LBpred p ->
- let logic_env = Logic_env.make profile in
- ignore (infer_predicate ~logic_env p);
- Ival Ival.zero_or_one
- | LBterm t' when LF_env.is_rec li ->
- let widened_profile = widen_profile profile in
- Widened_profile.add profile li widened_profile;
- (try LF_env.find li widened_profile
- with Not_found ->
- fixpoint ~infer li widened_profile t' (Ival Ival.bottom))
- | LBterm t' ->
- let logic_env = Logic_env.make profile in
- (* If the logic function returns a C type, then its application
- ranges inside this C type *)
- (match li.l_type with
- | Some (Ctype typ) ->
- ignore ((infer ~force ~logic_env t'));
- interv_of_typ typ;
- | None | Some (Linteger | Lreal | Ltype _ | Lvar _ | Larrow _) ->
- get_res (infer ~force ~logic_env t'))
- | _ -> assert false)
+ if LF_env.is_rec li then
+ let widened_profile = widen_profile profile in
+ Widened_profile.add profile li widened_profile;
+ (match li.l_body with
+ | LBpred p ->
+ LF_env.add_pred li widened_profile;
+ infer_predicate
+ ~logic_env:(Logic_env.make widened_profile) p;
+ Ival Ival.zero_or_one
+ | LBterm t' ->
+ (try LF_env.find li widened_profile
+ with Not_found ->
+ fixpoint ~infer li widened_profile t' (Ival Ival.bottom))
+ | _ -> assert false)
+ else
+ let logic_env = Logic_env.make profile in
+ (match li.l_body with
+ | LBpred p ->
+ ignore (infer_predicate ~logic_env p);
+ Ival Ival.zero_or_one
+ | LBterm t' ->
+ (* If the logic function returns a C type, then its application
+ ranges inside this C type *)
+ (match li.l_type with
+ | Some (Ctype typ) ->
+ ignore ((infer ~force ~logic_env t'));
+ interv_of_typ typ;
+ | None | Some (Linteger | Lreal | Ltype _ | Lvar _ | Larrow _) ->
+ get_res (infer ~force ~logic_env t'))
+ | _ -> assert false)
| LBnone when li.l_var_info.lv_name = "\\sum" ||
li.l_var_info.lv_name = "\\product" ->
(match args with
@@ -1011,15 +1019,22 @@ and infer_predicate ~logic_env p =
match p.pred_content with
| Pfalse | Ptrue -> ()
| Papp(li, _, args) ->
+ let profile =
+ Profile.make
+ li.l_profile
+ (List.map
+ (fun arg -> get_res (infer ~force:false ~logic_env arg))
+ args)
+ in
(match li.l_body with
+ | LBpred p when LF_env.is_rec li ->
+ let widened_profile = widen_profile profile in
+ Widened_profile.add profile li widened_profile;
+ (try ignore (LF_env.find li widened_profile)
+ with Not_found ->
+ LF_env.add_pred li widened_profile;
+ infer_predicate ~logic_env:(Logic_env.make widened_profile) p)
| LBpred p ->
- let profile =
- Profile.make
- li.l_profile
- (List.map
- (fun arg -> get_res (infer ~force:false ~logic_env arg))
- args)
- in
let logic_env = Logic_env.make profile in
ignore (infer_predicate ~logic_env p)
| LBnone -> ()
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index 88a168eb010bc49502d7fa635c930a9e3f5092fa..523a4eb5ca11bc61727d914b181166d2eea54322 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -208,6 +208,19 @@ end = struct
end
+module Recursive_pred : sig
+ val add: Profile.t -> logic_info -> unit
+ val is_done: Profile.t -> logic_info -> bool
+end = struct
+ let known = ref LFProf.Set.empty
+
+ let add profile li =
+ known := LFProf.Set.add (li, profile) !known
+
+ let is_done profile li = LFProf.Set.mem (li, profile) !known
+
+end
+
(******************************************************************************)
(** {2 Coercion rules} *)
(******************************************************************************)
@@ -558,6 +571,7 @@ let rec type_term
li.l_profile
(List.map (Interval.get_from_profile ~profile) args)
in
+ let new_profile = Interval.get_widened_profile new_profile li in
Stack.push
(fun () ->
ignore (type_predicate ~profile:new_profile p))
@@ -768,15 +782,20 @@ and type_predicate ~profile p =
begin
match li.l_body with
| LBpred p ->
- List.iter
- (fun x -> ignore (type_term ~use_gmp_opt: true ~profile x))
- args;
- let new_profile =
- Profile.make
- li.l_profile
- (List.map (Interval.get_from_profile ~profile) args)
- in
- type_predicate ~profile:new_profile p;
+ List.iter
+ (fun x -> ignore (type_term ~use_gmp_opt: true ~profile x))
+ args;
+ let new_profile =
+ Profile.make
+ li.l_profile
+ (List.map (Interval.get_from_profile ~profile) args)
+ in
+ let new_profile = Interval.get_widened_profile new_profile li in
+ if Recursive_pred.is_done new_profile li
+ then ()
+ else
+ (Recursive_pred.add new_profile li;
+ ignore (type_predicate ~profile:new_profile p))
| LBnone -> ()
| LBreads _ -> ()
| LBinductive _ -> ()