diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml
index d598f893bafdea3b5c687ff9eaf08ae0969e2f37..7e450eb7158254f94101c07eeae896c709e4f44e 100644
--- a/src/plugins/e-acsl/src/analyses/bound_variables.ml
+++ b/src/plugins/e-acsl/src/analyses/bound_variables.ml
@@ -731,7 +731,7 @@ end
method !vpredicate p =
let loc = p.pred_loc in
- match Predicate_normalizer.get p with
+ match Predicate_normalizer.get_pred p with
| PoT_pred p -> Error.generic_handle (process_quantif ~loc) () p;
Cil.DoChildren
| PoT_term _ -> Cil.DoChildren
diff --git a/src/plugins/e-acsl/src/analyses/predicate_normalizer.ml b/src/plugins/e-acsl/src/analyses/predicate_normalizer.ml
index 420768ebdf7899096001c547976dd67709818d79..8ff2f7c5a09e954edc8e3ac016ea0261a6b2e12c 100644
--- a/src/plugins/e-acsl/src/analyses/predicate_normalizer.ml
+++ b/src/plugins/e-acsl/src/analyses/predicate_normalizer.ml
@@ -41,29 +41,45 @@ module Id_predicate =
(* Memoization module which retrieves the preprocessed form of predicates *)
module Memo: sig
- val memo: (predicate -> pred_or_term option) -> predicate -> unit
- val get: predicate -> pred_or_term
+ val memo_pred: (predicate -> pred_or_term option) -> predicate -> unit
+ val get_pred: predicate -> pred_or_term
+ val memo_term : (term -> term option) -> term -> unit
+ val get_term : term -> term
val clear: unit -> unit
end = struct
- let tbl = Id_predicate.Hashtbl.create 97
+ let tbl_term = Misc.Id_term.Hashtbl.create 97
+ let tbl_pred = Id_predicate.Hashtbl.create 97
- let get p =
- try Id_predicate.Hashtbl.find tbl p
+ let get_pred p =
+ try Id_predicate.Hashtbl.find tbl_pred p
with Not_found -> Lscope.PoT_pred p
- let memo process p =
- try ignore (Id_predicate.Hashtbl.find tbl p) with
+ let memo_pred process p =
+ try ignore (Id_predicate.Hashtbl.find tbl_pred p) with
| Not_found ->
match process p with
- | Some pot -> Id_predicate.Hashtbl.add tbl p (pot)
+ | Some pot -> Id_predicate.Hashtbl.add tbl_pred p pot
| None -> ()
- let clear () = Id_predicate.Hashtbl.clear tbl
+ let get_term t =
+ try Misc.Id_term.Hashtbl.find tbl_term t
+ with Not_found -> t
+
+ let memo_term process t =
+ try ignore (Misc.Id_term.Hashtbl.find tbl_term t) with
+ | Not_found ->
+ match process t with
+ | Some term -> Misc.Id_term.Hashtbl.add tbl_term t term
+ | None -> ()
+
+ let clear () =
+ Misc.Id_term.Hashtbl.clear tbl_term;
+ Id_predicate.Hashtbl.clear tbl_pred
end
-let preprocess ~loc p =
+let preprocess_pred ~loc p =
match p.pred_content with
| Pvalid_read(BuiltinLabel Here as llabel, t)
| Pvalid(BuiltinLabel Here as llabel, t) -> begin
@@ -97,6 +113,28 @@ let preprocess ~loc p =
Some (Lscope.PoT_term tapp)
| _ -> None
+let preprocess_term ~loc t =
+ match t.term_node with
+ | Tapp(li, lst, [ t1; t2; {term_node = Tlambda([ k ], predicate)}])
+ when li.l_body = LBnone && li.l_var_info.lv_name = "\\numof" ->
+ let logic_info = Cil_const.make_logic_info "\\sum" in
+ logic_info.l_type <- li.l_type;
+ logic_info.l_tparams <- li.l_tparams;
+ logic_info.l_labels <- li.l_labels;
+ logic_info.l_profile <- li.l_profile;
+ logic_info.l_body <- li.l_body;
+ let conditional_term =
+ Logic_const.term ~loc
+ (Tif(predicate, Cil.lone (), Cil.lzero ())) Linteger
+ in
+ let lambda_term =
+ Logic_const.term ~loc (Tlambda([ k ], conditional_term)) Linteger
+ in
+ Some (Logic_const.term ~loc
+ (Tapp(logic_info, lst, [ t1; t2; lambda_term ])) Linteger)
+ | _ -> None
+
+
let preprocessor = object
inherit Visitor.frama_c_inplace
@@ -140,11 +178,15 @@ let preprocessor = object
| GText _
-> Cil.SkipChildren
- method !vpredicate p =
+ method !vpredicate p =
let loc = p.pred_loc in
- Memo.memo (preprocess ~loc) p;
+ Memo.memo_pred (preprocess_pred ~loc) p;
Cil.DoChildren
+ method !vterm t =
+ let loc = t.term_loc in
+ Memo.memo_term (preprocess_term ~loc) t;
+ Cil.DoChildren
end
let preprocess ast =
@@ -156,5 +198,6 @@ let preprocess_annot annot =
let preprocess_predicate p =
ignore (Visitor.visitFramacPredicate preprocessor p)
-let get = Memo.get
+let get_pred = Memo.get_pred
+let get_term = Memo.get_term
let clear = Memo.clear
diff --git a/src/plugins/e-acsl/src/analyses/predicate_normalizer.mli b/src/plugins/e-acsl/src/analyses/predicate_normalizer.mli
index 06f9a7d199f523f4910770686c438d6e2ed3faca..49654d41d6f8e0fd786c5aef35df856b8e32252e 100644
--- a/src/plugins/e-acsl/src/analyses/predicate_normalizer.mli
+++ b/src/plugins/e-acsl/src/analyses/predicate_normalizer.mli
@@ -41,7 +41,9 @@ val preprocess_annot : code_annotation -> unit
val preprocess_predicate : predicate -> unit
(** Preprocess a predicate and its children and store the results *)
-val get : predicate -> Lscope.pred_or_term
+val get_pred : predicate -> Lscope.pred_or_term
(** Retrieve the preprocessed form of a predicate *)
+val get_term : term -> term
+(** Retrieve the preprocessed form of a term *)
val clear: unit -> unit
(** clear the table of normalized predicates *)
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 448cba21c748a362471580206b36de98237956ab..618d4751d6a4401ceda25908c0816c71b6e0ff17 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -744,27 +744,9 @@ and context_insensitive_term_to_exp ~adata kf env t =
when li.l_body = LBnone && (li.l_var_info.lv_name = "\\sum" ||
li.l_var_info.lv_name = "\\product")->
extended_quantifier_to_exp ~adata ~loc kf env t t1 t2 lambda li.l_var_info
- | Tapp(li, lst, [ t1; t2; {term_node = Tlambda([ k ], predicate)}])
+ | Tapp(li, _, _)
when li.l_body = LBnone && li.l_var_info.lv_name = "\\numof" ->
- let logic_info = Cil_const.make_logic_info "\\sum" in
- logic_info.l_type <- li.l_type;
- logic_info.l_tparams <- li.l_tparams;
- logic_info.l_labels <- li.l_labels;
- logic_info.l_profile <- li.l_profile;
- logic_info.l_body <- li.l_body;
- let numof_as_sum =
- let conditional_term =
- Logic_const.term
- (Tif(predicate, Cil.lone (), Cil.lzero ())) Linteger
- in
- let lambda_term =
- Logic_const.term (Tlambda([ k ], conditional_term)) Linteger
- in
- (Logic_const.term
- (Tapp(logic_info, lst, [ t1; t2; lambda_term ])) Linteger)
- in
- Typing.type_term ~use_gmp_opt:true numof_as_sum;
- context_insensitive_term_to_exp ~adata kf env numof_as_sum
+ assert false
| Tapp(_, [], _) ->
let e, adata, env = Logic_functions.tapp_to_exp ~adata kf env t in
let adata, env = Assert.register_term ~loc kf env t e adata in
@@ -871,6 +853,7 @@ and term_to_exp ~adata kf env t =
environment '%a'"
Printer.pp_term t generate_rte Typing.Function_params_ty.pretty
(Env.Local_vars.get env);
+ let t = Predicate_normalizer.get_term t in
Extlib.flatten
(Env.with_rte_and_result env false
~f:(fun env ->
@@ -1242,7 +1225,7 @@ and predicate_content_to_exp ~adata ?name kf env p =
| Pfresh _ -> Env.not_yet env "\\fresh"
and predicate_to_exp ~adata ?name kf ?rte env p =
- match Predicate_normalizer.get p with
+ match Predicate_normalizer.get_pred p with
| PoT_term t -> term_to_exp ~adata kf env t
| PoT_pred p ->
let rte = match rte with None -> Env.generate_rte env | Some b -> b in