diff --git a/src/plugins/e-acsl/quantif.ml b/src/plugins/e-acsl/quantif.ml
index 3e42ca09557fdc9443ebb45e1109a59fe67fba8d..0bb9e0b55470392571b204ad8f95ecd2f5d07a05 100644
--- a/src/plugins/e-acsl/quantif.ml
+++ b/src/plugins/e-acsl/quantif.ml
@@ -181,6 +181,8 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
let env =
if Mpz.is_t ty then Env.add_stmt env (Mpz.init ~loc x) else env
in
+ let llv = cvar_to_lvar var_x in
+ if not (Mpz.is_t ty) then Typing.unsafe_unify ~from:logic_x llv;
(* build the inner loops and loop body *)
let body, env = mk_for_loop env tl in
(* initialize the loop counter to [t1] *)
@@ -194,7 +196,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
in
(* generate the guard [x bop t2] *)
let stmts_block b = [ mkStmt ~valid_sid:true (Block b) ] in
- let tlv = Logic_const.tvar ~loc (cvar_to_lvar var_x) in
+ let tlv = Logic_const.tvar ~loc llv in
let guard = Logic_const.term (TBinOp(bop2, tlv, t2)) Linteger in
Typing.type_term guard;
let guard_exp, env = term_to_exp (Env.push env) (Some intType) guard in
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
index cc1bdce74ad0760d34df778f5b3f85dc4341acb1..2f78b0c78335cf8821533a8c84a64f9d0990f771 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
@@ -79,11 +79,9 @@ int search(int elt)
while (1) {
if (__e_acsl_i < 9) { ; }
else { break; }
- e_acsl_assert((int)((long long)__e_acsl_i + (long long)1) < 10,
- (char *)"Precondition",
+ e_acsl_assert(__e_acsl_i + 1 < 10,(char *)"Precondition",
(char *)"index_bound: (int)(__e_acsl_i+1) < 10",9);
- e_acsl_assert(0 <= (int)((long long)__e_acsl_i + (long long)1),
- (char *)"Precondition",
+ e_acsl_assert(0 <= __e_acsl_i + 1,(char *)"Precondition",
(char *)"index_bound: 0 <= (int)(__e_acsl_i+1)",9);
e_acsl_assert(__e_acsl_i < 10,(char *)"Precondition",
(char *)"index_bound: __e_acsl_i < 10",9);
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index 18f953c1f7a3f03a0b4dc6b188f5e1fda5ce517e..dcc42fca248084f27b523733710887baa39973ec 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -46,6 +46,15 @@ type eacsl_typ =
| Z
| No_integral of logic_type
+(* debugging purpose only *)
+let _pretty_eacsl_typ fmt = function
+ | Interv(l, u) ->
+ Format.fprintf fmt "[ %a; %a ]"
+ (fun z -> Z.pretty z) l
+ (fun z -> Z.pretty z) u
+ | Z -> Format.fprintf fmt "Z"
+ | No_integral lty -> Format.fprintf fmt "%a" Cil.d_logic_type lty
+
exception Not_representable
let typ_of_integer i unsigned =
@@ -176,6 +185,14 @@ let unsafe_set_term t ty =
Term_env.add t (eacsl_typ_of_typ ty)
end
+let unsafe_unify ~from logic_v =
+ try
+ let ty = Logic_var_env.find from in
+ assert (not (Logic_var_env.mem logic_v));
+ Logic_var_env.add logic_v ty
+ with Not_found ->
+ Options.fatal "unknown logic variable %a" Cil.d_logic_var logic_v
+
let clear () =
Term_env.clear ();
Logic_var_env.clear ()
@@ -437,7 +454,8 @@ let type_term t = if not (Options.Gmp_only.get ()) then ignore (type_term t)
let type_named_predicate ?(must_clear=true) p =
if not (Options.Gmp_only.get ()) then begin
- Options.debug ~level:2 "typing predicate %a" Cil.d_predicate_named p;
+ Options.debug ~level:2 "typing predicate %a (clear? %b)"
+ Cil.d_predicate_named p must_clear;
if must_clear then clear ();
type_predicate_named p
end
@@ -515,7 +533,7 @@ C-representable@]";
let principal_type t1 t2 =
let ty1 = typ_of_term t1 in
let ty2 = typ_of_term t2 in
- (* possible to get an integralType (or Mpz.t) with a non-one in the case of
+ (* possible to get an integralType (or Mpz.t) from a non-one in the case of
\null *)
if Cil.isIntegralType ty1 then
if Cil.isIntegralType ty2 then Cil.arithmeticConversion ty1 ty2
diff --git a/src/plugins/e-acsl/typing.mli b/src/plugins/e-acsl/typing.mli
index d5f1279e487ea7b24bcf1c148f1124eec68213e0..9a3c57c24e33c892906dbe0b928f0344be3db4d7 100644
--- a/src/plugins/e-acsl/typing.mli
+++ b/src/plugins/e-acsl/typing.mli
@@ -45,6 +45,10 @@ val unsafe_set_term: term -> typ -> unit
(** Modify the type of the given term. No verification is done to check that the
new type is correct. *)
+val unsafe_unify: from:logic_var -> logic_var -> unit
+(** Set the type of the second logic var to the type of the first one, named
+ [from]. *)
+
val clear: unit -> unit
(** Remove all the previously computed types. *)
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index d4f061d60e78b008613560053feaee2a296d11e7..6d565ddd29c7ad6812c832568a7a005c479b536d 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -239,21 +239,25 @@ you must call function `%s' by yourself"
f)
method vglob_aux g =
- let is_library_var vi =
- List.mem (fst (vi.vdecl)).Lexing.pos_fname (Misc.library_files ())
+ (* TODO optimize: do not do the standard operation on library globals
+ without varinfo *)
+ let is_library_loc (loc, _) =
+ List.mem loc.Lexing.pos_fname (Misc.library_files ())
in
match g with
| GVarDecl(_, vi, _) | GVar(vi, _, _) | GFun({ svar = vi }, _)
- when is_library_var vi ->
+ when is_library_loc vi.vdecl ->
if generate then
Cil.JustCopyPost
(fun l ->
- Misc.register_library_function (Cil.get_varinfo self#behavior vi);
+ Misc.register_library_function (Cil.get_varinfo self#behavior vi);
l)
else begin
Misc.register_library_function vi;
Cil.SkipChildren
end
+ | g when is_library_loc (Global.loc g) ->
+ if generate then Cil.JustCopy else Cil.SkipChildren
| _ ->
let do_it = function
| GVar(vi, i, _) ->