From f9ad8534ad153e660e2a3a385b08f268a411881c Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 26 Jul 2019 15:40:10 +0200
Subject: [PATCH] [kernel] more appropriate locations for kernel functions
---
src/kernel_services/ast_data/globals.ml | 11 ++++-------
tests/spec/oracle/merge_bts938.res.oracle | 2 +-
tests/spec/oracle/multiple_decl_def_1.res.oracle | 2 +-
3 files changed, 6 insertions(+), 9 deletions(-)
diff --git a/src/kernel_services/ast_data/globals.ml b/src/kernel_services/ast_data/globals.ml
index efdc622fb24..dcf02526ae8 100644
--- a/src/kernel_services/ast_data/globals.ml
+++ b/src/kernel_services/ast_data/globals.ml
@@ -41,8 +41,7 @@ let get_locals f = match f.fundec with
| Declaration(_, _, _, _) -> []
let get_location kf = match kf.fundec with
- | Definition (_, loc) -> loc
- | Declaration (_,vi,_, _) -> vi.vdecl
+ | Definition (_, loc) | Declaration (_,_,_, loc) -> loc
let find_first_stmt = Extlib.mk_fun "Globals.find_first_stmt"
@@ -232,6 +231,7 @@ module Functions = struct
update_orig_name kf; kf)
let update_kf kf fundec spec =
+ let oldloc = get_location kf in
(match kf.fundec, fundec with
(* we never update a definition with a declaration (see bug 1914).
If you really want to play this game, just mutate the kf in place and
@@ -241,11 +241,8 @@ module Functions = struct
| _ -> kf.fundec <- fundec);
(* Kernel.feedback "UPDATE Spec of function %a (%a)"
Cil_datatype.Kf.pretty kf Printer.pp_funspec spec;*)
- let loc = match kf.fundec with
- | Definition (_, loc) | Declaration (_, _, _, loc) -> loc
- in
- let oldloc = Cil.CurrentLoc.get () in
- Cil.CurrentLoc.set loc;
+ (match fundec with
+ | Definition(_,loc) | Declaration(_,_,_,loc) -> CurrentLoc.set loc);
Logic_utils.merge_funspec ~oldloc kf.spec spec
let replace_by_declaration s v l=
diff --git a/tests/spec/oracle/merge_bts938.res.oracle b/tests/spec/oracle/merge_bts938.res.oracle
index 555761dbf9a..7601952cc83 100644
--- a/tests/spec/oracle/merge_bts938.res.oracle
+++ b/tests/spec/oracle/merge_bts938.res.oracle
@@ -6,7 +6,7 @@
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
+ found two contracts (old location: tests/spec/merge_bts938.h:2). Merging them
/* Generated by Frama-C */
extern int tab[10];
diff --git a/tests/spec/oracle/multiple_decl_def_1.res.oracle b/tests/spec/oracle/multiple_decl_def_1.res.oracle
index 0220fca8f25..a3057b3c95a 100644
--- a/tests/spec/oracle/multiple_decl_def_1.res.oracle
+++ b/tests/spec/oracle/multiple_decl_def_1.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing tests/spec/multiple_decl_def_1.c (with preprocessing)
[kernel] Parsing tests/spec/multiple_decl_def_2.c (with preprocessing)
[kernel] tests/spec/multiple_decl_def_2.c:5: Warning:
- found two contracts. Merging them
+ found two contracts (old location: tests/spec/multiple_decl_def_1.c:7). Merging them
/* Generated by Frama-C */
int f(int y);
--
GitLab