From 9f8d84d3c2bc599a68ac4d16251ba49c282d1c5e Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Tue, 23 Jul 2019 10:42:36 +0200
Subject: [PATCH] [Logic] include both locations in merge warnings
---
src/kernel_internals/typing/cabs2cil.ml | 10 +++--
src/kernel_services/ast_data/globals.ml | 3 +-
.../ast_queries/logic_utils.ml | 44 +++++++++++++------
.../ast_queries/logic_utils.mli | 11 +++--
tests/spec/oracle/merge_1.res.oracle | 3 +-
tests/spec/oracle/merge_bts938.res.oracle | 9 ++--
tests/spec/oracle/multiple_spec.res.oracle | 4 +-
...ibutes-declarations-definitions.res.oracle | 4 +-
tests/syntax/oracle/rettype.res.oracle | 3 +-
9 files changed, 59 insertions(+), 32 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 2dc94ecbea6..2a699d540db 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 b84dfc4a2b8..efdc622fb24 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 ff499c760d6..60c04c2d1f1 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 20f930b2b2f..02c25b8d0b4 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 c1506318808..3d7b10c4cf9 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 e4d80eb0bb7..9ae248d8d81 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 69741045383..36df4e03cdc 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 52cada7b775..936dd1c3300 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 d4b0fdb6a30..0b3783f2896 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.
--
GitLab