diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index acf13d03492d005669c9ee1afd15a7b2637e2cfb..18e4134ca9a8c25d63757652ba3ac2c604db9395 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,7 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
+- E-ACSL [2013/06/21] Fewer unknown locations.
-* E-ACSL [2013/06/18] Fixed bug when generating RTEs on the E-ACSL
generated project.
-* E-ACSL [2013/05/30] Fixed -e-acsl-debug n, with n >= 2.
diff --git a/src/plugins/e-acsl/env.ml b/src/plugins/e-acsl/env.ml
index c5aecb0631542b338dd94e26cef4a81d40d80e9f..13e6249ddf20d372ad050fc6f77633ee74fb4208 100644
--- a/src/plugins/e-acsl/env.ml
+++ b/src/plugins/e-acsl/env.ml
@@ -123,7 +123,7 @@ let generate_rte env =
(* eta-expansion required for typing generalisation *)
let acc_list_rev acc l = List.fold_left (fun acc x -> x :: acc) acc l
-let do_new_var ?loc init ?(global=false) ?(name="") env t ty mk_stmts =
+let do_new_var ~loc init ?(global=false) ?(name="") env t ty mk_stmts =
let local_env, tl_env = top init env in
let local_block = local_env.block_info in
let is_t = Mpz.is_t ty in
@@ -160,7 +160,7 @@ let do_new_var ?loc init ?(global=false) ?(name="") env t ty mk_stmts =
(* Options.feedback "memoizing %a for term %a"
Varinfo.pretty v (fun fmt t -> match t with None -> Format.fprintf fmt
"NONE" | Some t -> Term.pretty fmt t) t;*)
- { clear_stmts = Mpz.clear ?loc e :: tbl.clear_stmts;
+ { clear_stmts = Mpz.clear ~loc e :: tbl.clear_stmts;
new_exps = match t with
| None -> tbl.new_exps
| Some t -> Term.Map.add t (v, e) tbl.new_exps }
@@ -201,7 +201,7 @@ let do_new_var ?loc init ?(global=false) ?(name="") env t ty mk_stmts =
exception No_term
-let new_var ?loc ?(init=false) ?(global=false) ?name env t ty mk_stmts =
+let new_var ~loc ?(init=false) ?(global=false) ?name env t ty mk_stmts =
let local_env, _ = top init env in
let memo tbl =
try
@@ -211,7 +211,7 @@ let new_var ?loc ?(init=false) ?(global=false) ?name env t ty mk_stmts =
let v, e = Term.Map.find t tbl.new_exps in
if Typ.equal ty v.vtype then v, e, env else raise No_term
with Not_found | No_term ->
- do_new_var ?loc ~global init ?name env t ty mk_stmts
+ do_new_var ~loc ~global init ?name env t ty mk_stmts
in
if global then begin
assert (not init);
@@ -219,10 +219,10 @@ let new_var ?loc ?(init=false) ?(global=false) ?name env t ty mk_stmts =
end else
memo local_env.mpz_tbl
-let new_var_and_mpz_init ?loc ?init ?global ?name env t mk_stmts =
+let new_var_and_mpz_init ~loc ?init ?global ?name env t mk_stmts =
new_var
- ?loc ?init ?global ?name env t (Mpz.t ())
- (fun v e -> Mpz.init ?loc e :: mk_stmts v e)
+ ~loc ?init ?global ?name env t (Mpz.t ())
+ (fun v e -> Mpz.init ~loc e :: mk_stmts v e)
module Logic_binding = struct
@@ -241,7 +241,8 @@ module Logic_binding = struct
Error.not_yet msg
in
let v, e, env =
- new_var env ~name:logic_v.lv_name None ty (fun _ _ -> [])
+ new_var
+ ~loc:Location.unknown env ~name:logic_v.lv_name None ty (fun _ _ -> [])
in
v,
e,
diff --git a/src/plugins/e-acsl/env.mli b/src/plugins/e-acsl/env.mli
index bff818e26435ed1f20290584e02eebecea88e40f..e726c0bca128fbb7db42d71a19d6f5957b782b6b 100644
--- a/src/plugins/e-acsl/env.mli
+++ b/src/plugins/e-acsl/env.mli
@@ -36,7 +36,7 @@ val dummy: t
val empty: Visitor.frama_c_visitor -> t
val new_var:
- ?loc:location -> ?init:bool -> ?global:bool -> ?name:string ->
+ loc:location -> ?init:bool -> ?global:bool -> ?name:string ->
t -> term option -> typ ->
(varinfo -> exp (* the var as exp *) -> stmt list) ->
varinfo * exp * t
@@ -48,7 +48,7 @@ val new_var:
initialized by applying it to [mk_stmts]. *)
val new_var_and_mpz_init:
- ?loc:location -> ?init:bool -> ?global:bool -> ?name:string ->
+ loc:location -> ?init:bool -> ?global:bool -> ?name:string ->
t -> term option ->
(varinfo -> exp (* the var as exp *) -> stmt list) ->
varinfo * exp * t
diff --git a/src/plugins/e-acsl/misc.ml b/src/plugins/e-acsl/misc.ml
index a152d3128fa839606b52c38ce8fbf158b73e815b..2946037d24ffde555c65650eeaf4aca39c51f117 100644
--- a/src/plugins/e-acsl/misc.ml
+++ b/src/plugins/e-acsl/misc.ml
@@ -49,7 +49,7 @@ let reset () = Datatype.String.Hashtbl.clear library_functions
(** {2 Builders} *)
(* ************************************************************************** *)
-let mk_call ?(loc=Location.unknown) ?result fname args =
+let mk_call ~loc ?result fname args =
let vi =
try Datatype.String.Hashtbl.find library_functions fname
with Not_found -> Options.fatal "unregistered library function `%s'" fname
@@ -164,7 +164,7 @@ let mk_debug_mmodel_stmt stmt =
if Options.debug_atleast 1
&& Options.is_debug_key_enabled Options.dkey_analysis
then
- let debug = mk_call "__e_acsl_memory_debug" [] in
+ let debug = mk_call ~loc:(Stmt.loc stmt) "__e_acsl_memory_debug" [] in
Cil.mkStmt ~valid_sid:true (Block (Cil.mkBlock [ stmt; debug]))
else
stmt
diff --git a/src/plugins/e-acsl/misc.mli b/src/plugins/e-acsl/misc.mli
index 67bc74b0ab7811554237ab43f89d4819b0313021..450ede82e90d81b060418797a6154c1d2ee52960 100644
--- a/src/plugins/e-acsl/misc.mli
+++ b/src/plugins/e-acsl/misc.mli
@@ -29,7 +29,7 @@ open Cil_datatype
(** {2 Builders} *)
(* ************************************************************************** *)
-val mk_call: ?loc:Location.t -> ?result:lval -> string -> exp list -> stmt
+val mk_call: loc:Location.t -> ?result:lval -> string -> exp list -> stmt
val mk_debug_mmodel_stmt: stmt -> stmt
type annotation_kind =
diff --git a/src/plugins/e-acsl/mpz.ml b/src/plugins/e-acsl/mpz.ml
index 6dd1995b175a98d89bf5eb04db1a79889bc3f91f..c55a6d9d97eac5d915a112bff9c6b936f7c887f8 100644
--- a/src/plugins/e-acsl/mpz.ml
+++ b/src/plugins/e-acsl/mpz.ml
@@ -37,9 +37,9 @@ let is_now_referenced () = !t_torig_ref.treferenced <- true
let t () = TNamed(!t_torig_ref, [])
let is_t ty = Cil_datatype.Typ.equal ty (t ())
-let apply_on_var ?loc funname e = Misc.mk_call ?loc ("__gmpz_" ^ funname) [ e ]
-let init ?loc e = apply_on_var "init" ?loc e
-let clear ?loc e = apply_on_var "clear" ? loc e
+let apply_on_var ~loc funname e = Misc.mk_call ~loc ("__gmpz_" ^ funname) [ e ]
+let init ~loc e = apply_on_var "init" ~loc e
+let clear ~loc e = apply_on_var "clear" ~loc e
exception Longlong of ikind
@@ -62,16 +62,16 @@ let get_set_suffix_and_arg e =
[ e; Cil.integer ~loc:Location.unknown 10 ]
| _ -> assert false
-let generic_affect ?loc fname lv ev e =
+let generic_affect ~loc fname lv ev e =
let ty = Cil.typeOf ev in
if is_t ty then
let suf, args = get_set_suffix_and_arg e in
- Misc.mk_call ?loc (fname ^ suf) (ev :: args)
+ Misc.mk_call ~loc (fname ^ suf) (ev :: args)
else
- Cil.mkStmtOneInstr ~valid_sid:true (Set(lv, e, Location.unknown))
+ Cil.mkStmtOneInstr ~valid_sid:true (Set(lv, e, e.eloc))
-let init_set ?loc lv ev e =
- try generic_affect ?loc "__gmpz_init_set" lv ev e
+let init_set ~loc lv ev e =
+ try generic_affect ~loc "__gmpz_init_set" lv ev e
with
| Longlong IULongLong ->
(match e.enode with
@@ -79,14 +79,13 @@ let init_set ?loc lv ev e =
let call =
Misc.mk_call ?loc
"__gmpz_import"
- (let loc = match loc with None -> Location.unknown | Some l -> l in
- [ ev;
- Cil.one ~loc;
- Cil.one ~loc;
- Cil.sizeOf ~loc (TInt(IULongLong, []));
- Cil.zero ~loc;
- Cil.zero ~loc;
- Cil.mkAddrOf ~loc elv ])
+ [ ev;
+ Cil.one ~loc;
+ Cil.one ~loc;
+ Cil.sizeOf ~loc (TInt(IULongLong, []));
+ Cil.zero ~loc;
+ Cil.zero ~loc;
+ Cil.mkAddrOf ~loc elv ]
in
Cil.mkStmt
~valid_sid:true
@@ -95,8 +94,8 @@ let init_set ?loc lv ev e =
| Longlong ILongLong ->
Error.not_yet "long long requiring GMP"
-let affect ?loc lv ev e =
- try generic_affect ?loc "__gmpz_set" lv ev e
+let affect ~loc lv ev e =
+ try generic_affect ~loc "__gmpz_set" lv ev e
with Longlong _ ->
Error.not_yet "quantification over long long and requiring GMP"
diff --git a/src/plugins/e-acsl/mpz.mli b/src/plugins/e-acsl/mpz.mli
index 1b3be0da5ea5395e168ba8761e82d01cef778dc0..cebd5bbdac66a1fb3a1abf5d3a8ab932bbe3099c 100644
--- a/src/plugins/e-acsl/mpz.mli
+++ b/src/plugins/e-acsl/mpz.mli
@@ -35,17 +35,17 @@ val is_now_referenced: unit -> unit
val is_t: typ -> bool
(** is the type equal to "mpz_t"? *)
-val init: ?loc:location -> exp -> stmt
+val init: loc:location -> exp -> stmt
(** build stmt "mpz_init(v)" *)
-val init_set: ?loc:location -> lval -> exp -> exp -> stmt
+val init_set: loc:location -> lval -> exp -> exp -> stmt
(** [init_set x_as_lv x_as_exp e] builds stmt [x = e] or [mpz_init_set*(v, e)]
with the good function 'set' according to the type of e *)
-val clear: ?loc:location -> exp -> stmt
+val clear: loc:location -> exp -> stmt
(** build stmt "mpz_clear(v)" *)
-val affect: ?loc:location -> lval -> exp -> exp -> stmt
+val affect: loc:location -> lval -> exp -> exp -> stmt
(** [affect x_as_lv x_as_exp e] builds stmt [x = e] or [mpz_set*(e)] with the
good function 'set' according to the type of e *)
diff --git a/src/plugins/e-acsl/quantif.ml b/src/plugins/e-acsl/quantif.ml
index 392760003da19d6bfb25b1257fd5428e40dfe293..85d1cf3373c8383cfcfe6cdcf36e0e218cc12dfd 100644
--- a/src/plugins/e-acsl/quantif.ml
+++ b/src/plugins/e-acsl/quantif.ml
@@ -186,7 +186,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
let init_blk, env =
Env.pop_and_get
env
- (Mpz.affect lv_x x e1)
+ (Mpz.affect ~loc:e1.eloc lv_x x e1)
~global_clear:false
Env.Middle
in
@@ -217,7 +217,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
let next_blk, env =
Env.pop_and_get
env
- (Mpz.affect lv_x x incr)
+ (Mpz.affect ~loc:incr.eloc lv_x x incr)
~global_clear:false
Env.Middle
in
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index ee2a773aa3cb606dc446d9432b910ec27a1fd456..c7f6447d64adf8961aaf40fe55869dd80d2d1bd6 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -86,7 +86,7 @@ let name_of_mpz_arith_bop = function
| Lt | Gt | Le | Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr
| Shiftlt | Shiftrt | PlusPI | IndexPI | MinusPI | MinusPP -> assert false
-let constant_to_exp ?(loc=Location.unknown) = function
+let constant_to_exp ~loc = function
| Integer(n, s) ->
(try
let k = Typing.typ_of_integer n (Integer.ge n Integer.zero) in
@@ -401,8 +401,7 @@ and term_to_exp kf env ctx t =
(* generate the C code equivalent to [t1 bop t2]. *)
and comparison_to_exp
- ?(loc=Location.unknown) ?e1 kf env bop ?(name=name_of_binop bop)
- t1 t2 t_opt =
+ ~loc ?e1 kf env bop ?(name=name_of_binop bop) t1 t2 t_opt =
let e1, env, ctx = match e1 with
| None ->
let ctx = Typing.principal_type t1 t2 in
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index 0151681546e289610e4244aca60313054a9d30a5..774291da61d0c43dbfff27253bdfbab5bb5896ce 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -504,17 +504,17 @@ let type_named_predicate ?(must_clear=true) p =
(******************************************************************************)
(* convert [e] in a way that it is compatible with the given typing context. *)
-let context_sensitive ?loc ?name env ctx is_mpz_string t_opt e =
+let context_sensitive ~loc ?name env ctx is_mpz_string t_opt e =
let ty = Cil.typeOf e in
let mk_mpz e =
let _, e, env =
Env.new_var
- ?loc
+ ~loc
?name
env
t_opt
(Mpz.t ())
- (fun lv v -> [ Mpz.init_set ?loc (Cil.var lv) v e ])
+ (fun lv v -> [ Mpz.init_set ~loc (Cil.var lv) v e ])
in
e, env
in
@@ -529,7 +529,7 @@ let context_sensitive ?loc ?name env ctx is_mpz_string t_opt e =
"__gmpz_get_ui", Cil.ulongType
in
Options.warning
- ?source:(Extlib.opt_map fst loc)
+ ~source:(fst loc)
~once:true
"@[missing guard for ensuring that the given integer is \
C-representable@]";
diff --git a/src/plugins/e-acsl/typing.mli b/src/plugins/e-acsl/typing.mli
index ff1abf3ef5f2d59ca91043fcc3d33bb637742541..d70964e9b0543f90d24b86a2f4e845eea404c5b7 100644
--- a/src/plugins/e-acsl/typing.mli
+++ b/src/plugins/e-acsl/typing.mli
@@ -61,7 +61,7 @@ val principal_type: term -> term -> typ
contain both of them. Their types must have been previously computed. *)
val context_sensitive:
- ?loc:location -> ?name:string ->
+ loc:location -> ?name:string ->
Env.t -> typ -> bool -> term option -> exp -> exp * Env.t
(** [context_sensitive env ty is_mpz_string t_opt e] converts [e] in [env] in
such a way that it becomes usable in a context of type [ty]. [t_opt], if
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 76e61a7674a24026e2dad2684d1bbb1ddb508618..1bb2874ea2c024a9607b47349e15984c8d333b14 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -172,7 +172,7 @@ class e_acsl_visitor prj generate = object (self)
let e, env = self#literal_string env e in
let stmt =
Cil.mkStmtOneInstr ~valid_sid:true
- (Set(Cil.var new_vi, e, Location.unknown))
+ (Set(Cil.var new_vi, e, e.eloc))
in
model (stmt :: stmts), env)
global_vars
@@ -388,15 +388,16 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
inherit Cil.genericCilVisitor (Cil.copy_visit (Project.current ()))
method vexpr e = match e.enode with
| Const(CStr s) ->
+ let loc = e.eloc in
let _, exp, env =
Env.new_var
+ ~loc
~global:true
~name:"literal_string"
env
None
Cil.charPtrType
(fun vi _ ->
- let loc = e.eloc in
let str_size = Cil.new_exp loc (SizeOfStr s) in
[ Cil.mkStmtOneInstr
~valid_sid:true (Set(Cil.var vi, e, loc));