diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml
index 28581fd29080aeaa60b201349e649738441220b9..f6fa2398373722c71c9d19af4976ec3348bebe63 100644
--- a/src/plugins/e-acsl/src/analyses/bound_variables.ml
+++ b/src/plugins/e-acsl/src/analyses/bound_variables.ml
@@ -688,17 +688,25 @@ end
| Pexists _ -> Error.not_yet "unguarded \\exists quantification"
| _ -> ()
- let preprocessor = object
- inherit E_acsl_visitor.visitor
+ let gannot a =
+ match a with
+ | Dfun_or_pred (li,loc) ->
+ (match li.l_body with
+ | LBpred p ->
+ (match Logic_normalizer.get_pred p with
+ | PoT_pred p -> process_quantif ~loc p
+ | PoT_term _ -> ())
+ | _ -> ())
+
+ | _ -> ()
- (* Only logic functions and logic predicates are handled.
- E-acsl simply ignores all the other global annotations *)
- method !vannotation annot =
- match annot with
- | Dfun_or_pred _ -> Cil.DoChildren
- | _ -> Cil.SkipChildren
+ let do_predicates () =
+ Annotations.iter_global (fun _ a -> gannot a)
+
+ let preprocessor = object
+ inherit E_acsl_visitor.visitor
- method !vpredicate p =
+ method !vpredicate p =
let loc = p.pred_loc in
match Logic_normalizer.get_pred p with
| PoT_pred p -> process_quantif ~loc p;
@@ -710,7 +718,8 @@ end
let compute ast =
Visitor.visitFramacFileSameGlobals
(preprocessor :> Visitor.frama_c_inplace)
- ast
+ ast;
+ do_predicates ()
let compute_annot annot =
ignore
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index 0234137c76103a4d35bc3c5a38a8d975d1b90162..e1e24001f371146b30863ea87f39a310e5195466 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -926,10 +926,10 @@ let type_named_predicate ?(lenv=[]) p =
Stack.pop pending_typing ()
done
-let unsafe_set t ?ctx ty =
+let unsafe_set t ?ctx ?(lenv=[]) ty =
let ctx = match ctx with None -> ty | Some ctx -> ctx in
let mk _ = coerce ~arith_operand:false ~ctx ~op:ty ty in
- ignore (Memo.memo mk t)
+ ignore (Memo.memo mk ~lenv t)
(******************************************************************************)
(** {2 Getters} *)
diff --git a/src/plugins/e-acsl/src/analyses/typing.mli b/src/plugins/e-acsl/src/analyses/typing.mli
index f6b783cf0cdd3798fbe76fc148235e374caccb7d..84e1a12d2af7c05a614cc195796062a277a721ae 100644
--- a/src/plugins/e-acsl/src/analyses/typing.mli
+++ b/src/plugins/e-acsl/src/analyses/typing.mli
@@ -144,7 +144,12 @@ val get_cast: lenv:Function_params_ty.t -> term -> typ option
val get_cast_of_predicate: lenv:Function_params_ty.t -> predicate -> typ option
(** Like {!get_cast}, but for predicates. *)
-val unsafe_set: term -> ?ctx:number_ty -> number_ty -> unit
+val unsafe_set:
+ term ->
+ ?ctx:number_ty ->
+ ?lenv:Function_params_ty.t ->
+ number_ty ->
+ unit
(** Register that the given term has the given type in the given context (if
any). No verification is done. *)
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index 28f9cc13914766a32aa85b68c6a78811ce9a9f49..340f645951c9e4e5c44579661253ed102b722f4f 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -65,7 +65,7 @@ let handle_annotations env kf stmt =
| Some (t, measure_opt) ->
let env = Env.set_annotation_kind env Smart_stmt.Variant in
let env = Env.push env in
- Typing.type_term ~use_gmp_opt:true t;
+ Typing.type_term ~use_gmp_opt:true ~lenv:(Env.Local_vars.get env) t;
let ty = Typing.get_typ ~lenv:(Env.Local_vars.get env) t in
if Gmp_types.is_t ty then Error.not_yet "loop variant using GMP";
let e, _, env = !term_to_exp_ref ~adata:Assert.no_data kf env t in
@@ -106,7 +106,10 @@ let handle_annotations env kf stmt =
term_name = [];
term_type = Linteger;}
in
- Typing.type_term ~use_gmp_opt:true tapp;
+ Typing.type_term
+ ~use_gmp_opt:true
+ ~lenv:(Env.Local_vars.get env)
+ tapp;
let e, _, env = !term_to_exp_ref ~adata:Assert.no_data kf env t in
let e_tapp, _, env =
Logic_functions.app_to_exp
@@ -166,7 +169,9 @@ let handle_annotations env kf stmt =
let variant_pos =
Logic_const.prel ~loc (Rge, t_old, Logic_const.tinteger ~loc 0)
in
- Typing.type_named_predicate variant_pos;
+ Typing.type_named_predicate
+ ~lenv:(Env.Local_vars.get env)
+ variant_pos;
let variant_pos_e, _, env =
!predicate_to_exp_ref ~adata:Assert.no_data kf env variant_pos
in
@@ -200,7 +205,9 @@ let handle_annotations env kf stmt =
let variant_dec =
Logic_const.prel ~loc (Rgt, t_old, t)
in
- Typing.type_named_predicate variant_dec;
+ Typing.type_named_predicate
+ ~lenv:(Env.Local_vars.get env)
+ variant_dec;
let variant_dec_e, _, env =
!predicate_to_exp_ref ~adata:Assert.no_data kf env variant_dec
in
@@ -288,8 +295,8 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
mk_innermost_block env
| Lscope.Lvs_quantif(t1, rel1, logic_x, rel2, t2) :: lscope_vars' ->
assert (rel1 == Rle && rel2 == Rlt);
- Typing.type_term ~use_gmp_opt:false t1;
- Typing.type_term ~use_gmp_opt:false t2;
+ Typing.type_term ~use_gmp_opt:false ~lenv:(Env.Local_vars.get env) t1;
+ Typing.type_term ~use_gmp_opt:false ~lenv:(Env.Local_vars.get env) t2;
let ctx =
let ty1 = Typing.get_number_ty ~lenv:(Env.Local_vars.get env) t1 in
let ty2 = Typing.get_number_ty ~lenv:(Env.Local_vars.get env) t2 in
@@ -301,9 +308,9 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
let res = Logic_const.term ~loc (TBinOp(PlusA, t, tone)) Linteger in
Option.iter
(fun ty ->
- Typing.unsafe_set tone ~ctx:ty ctx;
- Typing.unsafe_set t ~ctx:ty ctx;
- Typing.unsafe_set res ty)
+ Typing.unsafe_set tone ~ctx:ty ~lenv:(Env.Local_vars.get env) ctx;
+ Typing.unsafe_set t ~ctx:ty ~lenv:(Env.Local_vars.get env) ctx;
+ Typing.unsafe_set res ~lenv:(Env.Local_vars.get env) ty)
ty;
res
in
@@ -348,7 +355,11 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
(TBinOp(Lt, tlv, { t2 with term_node = t2.term_node } ))
Linteger
in
- Typing.type_term ~use_gmp_opt:false ~ctx:Typing.c_int guard;
+ Typing.type_term
+ ~use_gmp_opt:false
+ ~lenv:(Env.Local_vars.get env)
+ ~ctx:Typing.c_int
+ guard;
let guard_exp, _, env = term_to_exp kf (Env.push env) guard in
let break_stmt = Smart_stmt.break ~loc:guard_exp.eloc in
let guard_blk, env = Env.pop_and_get