diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 2dc94ecbea6e266a271437777a85c622515f19bc..2a699d540db7202d39de0fbd85917451f391ad73 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -742,9 +742,9 @@ let update_fundec_in_theFile vi (f:global -> unit) =
let update_funspec_in_theFile vi spec =
let rec aux = function
| [] -> assert false
- | GFun (f,_) :: _ ->
+ | GFun (f,oldloc) :: _ ->
Cil.CurrentLoc.set vi.vdecl;
- Logic_utils.merge_funspec f.sspec spec
+ Logic_utils.merge_funspec ~oldloc f.sspec spec
| _ :: tl -> aux tl
in
aux (findVarInTheFile vi)
@@ -8443,8 +8443,9 @@ and createGlobal ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool * A
msg vi.vname;
empty_funspec ()
in
+ let oldloc = Cil.CurrentLoc.get () in
Cil.CurrentLoc.set vi.vdecl;
- Logic_utils.merge_funspec old_spec spec
+ Logic_utils.merge_funspec ~oldloc old_spec spec
| _ -> assert false
in
update_fundec_in_theFile vi merge_spec
@@ -9065,12 +9066,13 @@ and doDecl local_env (isglobal: bool) : A.definition -> chunk = function
end;
(* Merge pre-existing spec if needed. *)
if has_decl then begin
+ let oldloc = CurrentLoc.get () in
let merge_spec = function
| GFunDecl(old_spec,_,loc) as g ->
if not (Cil.is_empty_funspec old_spec) then begin
rename_spec g;
Cil.CurrentLoc.set loc;
- Logic_utils.merge_funspec
+ Logic_utils.merge_funspec ~oldloc
!currentFunctionFDEC.sspec old_spec;
Logic_utils.clear_funspec old_spec;
end
diff --git a/src/kernel_services/ast_data/globals.ml b/src/kernel_services/ast_data/globals.ml
index b84dfc4a2b8b68eda18195b19b57f12e2468b223..efdc622fb24eaf36280faacc755335f25a5cf6b0 100644
--- a/src/kernel_services/ast_data/globals.ml
+++ b/src/kernel_services/ast_data/globals.ml
@@ -244,8 +244,9 @@ module Functions = struct
let loc = match kf.fundec with
| Definition (_, loc) | Declaration (_, _, _, loc) -> loc
in
+ let oldloc = Cil.CurrentLoc.get () in
Cil.CurrentLoc.set loc;
- Logic_utils.merge_funspec kf.spec spec
+ Logic_utils.merge_funspec ~oldloc kf.spec spec
let replace_by_declaration s v l=
(* Kernel.feedback "replacing %a by decl" Cil_datatype.Varinfo.pretty v;*)
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index ff499c760d6de4c292557b209eddd1709cacca0b..60c04c2d1f1c27fc58504799c98c9d865bac9522 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -1923,7 +1923,14 @@ let merge_post_cond l1 l2 =
else pc::acc)
l1 l2
-let merge_behaviors ~silent old_behaviors fresh_behaviors =
+let pp_old_loc fmt oldloc =
+ if Cil_datatype.Location.(equal oldloc unknown) then
+ Format.ifprintf fmt ""
+ else
+ Format.fprintf fmt " (old location: %a)"
+ Cil_datatype.Location.pretty oldloc
+
+let merge_behaviors ?(oldloc=Cil_datatype.Location.unknown) ~silent old_behaviors fresh_behaviors =
old_behaviors @
(List.filter
(fun b ->
@@ -1931,26 +1938,33 @@ let merge_behaviors ~silent old_behaviors fresh_behaviors =
let old_b = List.find (fun x -> x.b_name = b.b_name) old_behaviors in
if not (is_same_behavior b old_b) then begin
if not silent then
- Kernel.warning ~current:true "found two %s. Merging them%t"
+ let curloc = CurrentLoc.get () in
+ let source =
+ if Cil_datatype.Location.(equal oldloc unknown) then fst curloc
+ else fst oldloc
+ in
+ Kernel.warning ~source "found two %s%a. Merging them%t"
(if Cil.is_default_behavior b then "contracts"
else "behaviors named " ^ b.b_name)
+ pp_old_loc (if Cil_datatype.Position.equal source (fst curloc)
+ then Cil_datatype.Location.unknown else curloc)
(fun fmt ->
if Kernel.debug_atleast 1 then
Format.fprintf fmt ":@ @[%a@] vs. @[%a@]"
Cil_printer.pp_behavior b Cil_printer.pp_behavior old_b)
- ;
- old_b.b_assumes <- merge_ip_list old_b.b_assumes b.b_assumes;
- old_b.b_requires <- merge_ip_list old_b.b_requires b.b_requires;
- old_b.b_post_cond <-
- merge_post_cond old_b.b_post_cond b.b_post_cond;
- old_b.b_assigns <- merge_assigns old_b.b_assigns b.b_assigns;
- old_b.b_allocation <- merge_allocation old_b.b_allocation b.b_allocation;
+ ;
+ old_b.b_assumes <- merge_ip_list old_b.b_assumes b.b_assumes;
+ old_b.b_requires <- merge_ip_list old_b.b_requires b.b_requires;
+ old_b.b_post_cond <-
+ merge_post_cond old_b.b_post_cond b.b_post_cond;
+ old_b.b_assigns <- merge_assigns old_b.b_assigns b.b_assigns;
+ old_b.b_allocation <- merge_allocation old_b.b_allocation b.b_allocation;
end ;
false
with Not_found -> true)
fresh_behaviors)
-let merge_funspec ?(silent_about_merging_behav=false) old_spec fresh_spec =
+let merge_funspec ?(oldloc=Cil_datatype.Location.unknown) ?(silent_about_merging_behav=false) old_spec fresh_spec =
if not (is_same_spec old_spec fresh_spec || Cil.is_empty_funspec fresh_spec)
then
if Cil.is_empty_funspec old_spec then begin
@@ -1961,7 +1975,7 @@ let merge_funspec ?(silent_about_merging_behav=false) old_spec fresh_spec =
old_spec.spec_variant <- fresh_spec.spec_variant;
end else begin
old_spec.spec_behavior <-
- merge_behaviors ~silent:silent_about_merging_behav
+ merge_behaviors ~oldloc ~silent:silent_about_merging_behav
old_spec.spec_behavior fresh_spec.spec_behavior ;
(match old_spec.spec_variant,fresh_spec.spec_variant with
| None,None -> ()
@@ -1969,14 +1983,16 @@ let merge_funspec ?(silent_about_merging_behav=false) old_spec fresh_spec =
| None, Some _ -> old_spec.spec_variant <- fresh_spec.spec_variant
| Some _old, Some _fresh ->
Kernel.warning ~current:true
- "found two variants for function specification. Keeping only the first one.");
+ "found two variants for function specification%a. Keeping only the first one."
+ pp_old_loc oldloc);
(match old_spec.spec_terminates, fresh_spec.spec_terminates with
| None, None -> ()
| Some p1, Some p2 when is_same_identified_predicate p1 p2 -> ()
| _ ->
Kernel.warning ~current:true
- "found two different terminates clause for function specification. \
- keeping only the fist one");
+ "found two different terminates clauses for function specification%a. \
+ keeping only the fist one"
+ pp_old_loc oldloc);
old_spec.spec_complete_behaviors <-
List.fold_left (fun acc b ->
if List.mem b old_spec.spec_complete_behaviors then acc
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index 20f930b2b2f32927c1a016cafbea995c1e121da7..02c25b8d0b4ed95c523a3167c8ba3b2b78ab6e58 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -362,13 +362,16 @@ val concat_allocation: allocation -> allocation -> allocation
val merge_allocation : allocation -> allocation -> allocation
val merge_behaviors :
- silent:bool -> funbehavior list -> funbehavior list -> funbehavior list
+ ?oldloc:Cil_types.location -> silent:bool -> funbehavior list -> funbehavior list -> funbehavior list
-(** [merge_funspec oldspec newspec] merges [newspec] into [oldspec].
+(** [merge_funspec ?oldloc oldspec newspec] merges [newspec] into [oldspec].
If the funspec belongs to a kernel function, do not forget to call
- {!Kernel_function.set_spec} after merging. *)
+ {!Kernel_function.set_spec} after merging.
+ @modify Frama-C+dev add optional parameter [oldloc].
+*)
val merge_funspec :
- ?silent_about_merging_behav:bool -> funspec -> funspec -> unit
+ ?oldloc:Cil_types.location -> ?silent_about_merging_behav:bool ->
+ funspec -> funspec -> unit
(** Reset the given funspec to empty.
@since Nitrogen-20111001 *)
diff --git a/tests/spec/oracle/merge_1.res.oracle b/tests/spec/oracle/merge_1.res.oracle
index c1506318808a1a8ef1fca14c72352787fe8d9d44..3d7b10c4cf91f7ca6628a47a23a3bc603fef623c 100644
--- a/tests/spec/oracle/merge_1.res.oracle
+++ b/tests/spec/oracle/merge_1.res.oracle
@@ -1,6 +1,7 @@
[kernel] Parsing tests/spec/merge_1.i (no preprocessing)
[kernel] Parsing tests/spec/merge_2.i (no preprocessing)
-[kernel] tests/spec/merge_2.i:4: Warning: found two contracts. Merging them
+[kernel] tests/spec/merge_2.i:10: Warning:
+ found two contracts (old location: tests/spec/merge_2.i:4). Merging them
/* Generated by Frama-C */
int slen(char const *str);
diff --git a/tests/spec/oracle/merge_bts938.res.oracle b/tests/spec/oracle/merge_bts938.res.oracle
index e4d80eb0bb7e027ac7f545838fd6b7849743be49..9ae248d8d815de6976c833d3c683759a6aed2ab2 100644
--- a/tests/spec/oracle/merge_bts938.res.oracle
+++ b/tests/spec/oracle/merge_bts938.res.oracle
@@ -1,9 +1,12 @@
[kernel] Parsing tests/spec/merge_bts938.c (with preprocessing)
-[kernel] tests/spec/merge_bts938.h:2: Warning: found two contracts. Merging them
+[kernel] tests/spec/merge_bts938.c:7: Warning:
+ found two contracts (old location: tests/spec/merge_bts938.h:2). Merging them
[kernel] Parsing tests/spec/merge_bts938_1.c (with preprocessing)
-[kernel] tests/spec/merge_bts938.h:3: Warning: found two contracts. Merging them
-[kernel] tests/spec/merge_bts938.c:8: Warning: found two contracts. Merging them
+[kernel] tests/spec/merge_bts938_1.c:7: Warning:
+ found two contracts (old location: tests/spec/merge_bts938.h:3). Merging them
[kernel] tests/spec/merge_bts938.c:8: Warning: found two contracts. Merging them
+[kernel] tests/spec/merge_bts938.c:8: Warning:
+ found two contracts (old location: tests/spec/merge_bts938.c:8). Merging them
/* Generated by Frama-C */
extern int tab[10];
diff --git a/tests/spec/oracle/multiple_spec.res.oracle b/tests/spec/oracle/multiple_spec.res.oracle
index 69741045383095161745255fe0e7649886b6d0ef..36df4e03cdcd5ffdde70995a0046ae7e241ac7d4 100644
--- a/tests/spec/oracle/multiple_spec.res.oracle
+++ b/tests/spec/oracle/multiple_spec.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/spec/multiple_spec.c (with preprocessing)
-[kernel] tests/spec/multiple_spec.c:4: Warning:
- found two contracts. Merging them
+[kernel] tests/spec/multiple_spec.c:6: Warning:
+ found two contracts (old location: tests/spec/multiple_spec.c:4). Merging them
/* Generated by Frama-C */
/*@ requires y ≥ 0;
requires y ≤ 0; */
diff --git a/tests/syntax/oracle/attributes-declarations-definitions.res.oracle b/tests/syntax/oracle/attributes-declarations-definitions.res.oracle
index 52cada7b7752aba80dfc8e145419f29b41a97db7..936dd1c330043ea095b108662390a75dc834fcb5 100644
--- a/tests/syntax/oracle/attributes-declarations-definitions.res.oracle
+++ b/tests/syntax/oracle/attributes-declarations-definitions.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/syntax/attributes-declarations-definitions.c (with preprocessing)
-[kernel] tests/syntax/attributes-declarations-definitions.c:1: Warning:
- found two contracts. Merging them
+[kernel] tests/syntax/attributes-declarations-definitions.c:7: Warning:
+ found two contracts (old location: tests/syntax/attributes-declarations-definitions.c:1). Merging them
[kernel] tests/syntax/attributes-declarations-definitions.c:8: Warning:
found two contracts. Merging them
/* Generated by Frama-C */
diff --git a/tests/syntax/oracle/rettype.res.oracle b/tests/syntax/oracle/rettype.res.oracle
index d4b0fdb6a306ec9604f24d60ded231f3af15e64c..0b3783f28964f90407a67e0aca5c947569388b7d 100644
--- a/tests/syntax/oracle/rettype.res.oracle
+++ b/tests/syntax/oracle/rettype.res.oracle
@@ -2,6 +2,7 @@
[kernel] tests/syntax/rettype.i:8: User Error:
Declaration of foo does not match previous declaration from tests/syntax/rettype.i:5 (different integer types:
'int' and 'unsigned short').
-[kernel] tests/syntax/rettype.i:4: Warning: found two contracts. Merging them
+[kernel] tests/syntax/rettype.i:7: Warning:
+ found two contracts (old location: tests/syntax/rettype.i:4). Merging them
[kernel] User Error: stopping on file "tests/syntax/rettype.i" that has errors.
[kernel] Frama-C aborted: invalid user input.