From 3fe018a62cef45f56f4fc44ba73bd33d92076f06 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 24 Jul 2019 18:04:51 +0200
Subject: [PATCH] [kernel] oldloc means oldloc, currentloc means currentloc
---
src/kernel_internals/typing/cabs2cil.ml | 9 ++-----
.../ast_queries/logic_utils.ml | 24 +++----------------
tests/spec/oracle/merge_bts938.res.oracle | 2 +-
tests/spec/oracle/multiple_spec.res.oracle | 2 +-
...ibutes-declarations-definitions.res.oracle | 4 ++--
5 files changed, 9 insertions(+), 32 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 2a699d540db..cd3d07b4f50 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -743,7 +743,6 @@ let update_funspec_in_theFile vi spec =
let rec aux = function
| [] -> assert false
| GFun (f,oldloc) :: _ ->
- Cil.CurrentLoc.set vi.vdecl;
Logic_utils.merge_funspec ~oldloc f.sspec spec
| _ :: tl -> aux tl
in
@@ -8430,7 +8429,7 @@ and createGlobal ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool * A
| Some (spec,loc) ->
CurrentLoc.set loc;
let merge_spec = function
- | GFunDecl(old_spec, _, _) ->
+ | GFunDecl(old_spec, _, oldloc) ->
let behaviors =
List.map (fun b -> b.b_name) old_spec.spec_behavior
in
@@ -8443,8 +8442,6 @@ 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 ~oldloc old_spec spec
| _ -> assert false
in
@@ -9066,12 +9063,10 @@ 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 ->
+ | GFunDecl(old_spec,_,oldloc) as g ->
if not (Cil.is_empty_funspec old_spec) then begin
rename_spec g;
- Cil.CurrentLoc.set loc;
Logic_utils.merge_funspec ~oldloc
!currentFunctionFDEC.sspec old_spec;
Logic_utils.clear_funspec old_spec;
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 54b68435ee9..d871d6dd804 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -1938,13 +1938,7 @@ let merge_behaviors ?(oldloc=Cil_datatype.Location.unknown) ~silent old_behavior
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
- let curloc = CurrentLoc.get () in
- let source, oldloc =
- if Cil_datatype.Location.(equal oldloc unknown) then
- fst curloc, oldloc
- else fst oldloc, curloc
- in
- Kernel.warning ~source "found two %s%a. Merging them%t"
+ Kernel.warning ~current:true "found two %s%a. Merging them%t"
(if Cil.is_default_behavior b then "contracts"
else "behaviors named " ^ b.b_name)
pp_old_loc oldloc
@@ -1982,13 +1976,7 @@ let merge_funspec ?(oldloc=Cil_datatype.Location.unknown) ?(silent_about_merging
| Some _, None -> ()
| None, Some _ -> old_spec.spec_variant <- fresh_spec.spec_variant
| Some _old, Some _fresh ->
- let curloc = CurrentLoc.get() in
- let source, oldloc =
- if Cil_datatype.Location.(equal oldloc unknown) then
- fst curloc, oldloc
- else fst oldloc, curloc
- in
- Kernel.warning ~source
+ Kernel.warning ~current:true
"found two variants for function specification%a. \
Keeping only the first one."
pp_old_loc oldloc);
@@ -1996,13 +1984,7 @@ let merge_funspec ?(oldloc=Cil_datatype.Location.unknown) ?(silent_about_merging
| None, None -> ()
| Some p1, Some p2 when is_same_identified_predicate p1 p2 -> ()
| _ ->
- let curloc = CurrentLoc.get() in
- let source, oldloc =
- if Cil_datatype.Location.(equal oldloc unknown) then
- fst curloc, oldloc
- else fst oldloc, curloc
- in
- Kernel.warning ~source
+ Kernel.warning ~current:true
"found two different terminates clauses \
for function specification%a. Keeping only the first one"
pp_old_loc oldloc);
diff --git a/tests/spec/oracle/merge_bts938.res.oracle b/tests/spec/oracle/merge_bts938.res.oracle
index 9ae248d8d81..555761dbf9a 100644
--- a/tests/spec/oracle/merge_bts938.res.oracle
+++ b/tests/spec/oracle/merge_bts938.res.oracle
@@ -3,7 +3,7 @@
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_1.c:7: Warning:
- found two contracts (old location: tests/spec/merge_bts938.h:3). Merging them
+ found two contracts (old location: tests/spec/merge_bts938.h:2). 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
diff --git a/tests/spec/oracle/multiple_spec.res.oracle b/tests/spec/oracle/multiple_spec.res.oracle
index 36df4e03cdc..36031750dea 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:6: Warning:
- found two contracts (old location: tests/spec/multiple_spec.c:4). Merging them
+ found two contracts (old location: tests/spec/multiple_spec.c:3). 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 936dd1c3300..196ad631a7a 100644
--- a/tests/syntax/oracle/attributes-declarations-definitions.res.oracle
+++ b/tests/syntax/oracle/attributes-declarations-definitions.res.oracle
@@ -1,8 +1,8 @@
[kernel] Parsing tests/syntax/attributes-declarations-definitions.c (with preprocessing)
[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
+[kernel] tests/syntax/attributes-declarations-definitions.c:16: Warning:
+ found two contracts (old location: tests/syntax/attributes-declarations-definitions.c:8). Merging them
/* Generated by Frama-C */
typedef int __attribute__((__a1__)) aint;
typedef int __attribute__((__p1__)) * __attribute__((__p2__)) iptr;
--
GitLab