diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index ae2431695307561dd157c601799117b5f6650c4f..d113d0f789df3390a8117d96dfd7ebe794e2a0dd 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -1854,7 +1854,7 @@ type syntactic_scope =
@since Frama-C+dev
*)
| Block_scope of stmt
- (** globals + all locals of the blocks to which the given statement
+ (** locals (including static locals) of the block to which the given statement
belongs. *)
| Whole_function of kernel_function
(** same as above, but any local variable of the given function, regardless of
diff --git a/src/kernel_services/ast_data/globals.ml b/src/kernel_services/ast_data/globals.ml
index 979aed0a1fe46383ac61c6f41fac5a2f76f24732..4211f7a067776bf54e2f4dc46c3d19f18713bbf7 100644
--- a/src/kernel_services/ast_data/globals.ml
+++ b/src/kernel_services/ast_data/globals.ml
@@ -43,6 +43,8 @@ let get_locals f = match f.fundec with
let get_location kf = match kf.fundec with
| Definition (_, loc) | Declaration (_,_,_, loc) -> loc
+let get_statics = Extlib.mk_fun "Globals.get_statics"
+
let find_first_stmt = Extlib.mk_fun "Globals.find_first_stmt"
let find_enclosing_block = Extlib.mk_fun "Globals.find_enclosing_block"
@@ -94,7 +96,7 @@ module Vars = struct
v.vname = name &&
Filepath.Normalized.equal file (fst v.vdecl).pos_path)
| Whole_function kf ->
- List.find (fun v -> v.vname = name) (get_locals kf)
+ List.find (fun v -> v.vname = name) (get_locals kf @ !get_statics kf)
| Formal kf ->
List.find (fun v -> v.vname = name) (get_formals kf)
| Block_scope stmt ->
@@ -647,8 +649,8 @@ end
module Syntactic_search = struct
module Key =
- Datatype.Pair_with_collections
- (Datatype.String)(Cil_datatype.Syntactic_scope)
+ Datatype.Triple_with_collections
+ (Datatype.String)(Cil_datatype.Syntactic_scope)(Datatype.Bool)
(struct let module_name = "Globals.Datatype.Key" end)
module Scope_info =
@@ -664,12 +666,18 @@ module Syntactic_search = struct
let () = Ast.add_monotonic_state self
- let rec find_var (x,scope) =
+ let rec find_var (x,scope,strict) =
let has_name v = v.vorig_name = x in
let global_has_name v =
has_name v && v.vglob
&& not (Cil.hasAttribute Cabs2cil.fc_local_static v.vattr)
in
+ let lookup next_scope candidate =
+ match candidate with
+ | Some _ -> candidate
+ | None when strict -> candidate
+ | None -> find_in_scope x next_scope
+ in
let module M = struct exception Found of varinfo end in
match scope with
| Global ->
@@ -683,11 +691,15 @@ module Syntactic_search = struct
None
with M.Found v -> Some v)
| Translation_unit file ->
- let symbols = FileIndex.get_globals file in
- (try Some (fst (List.find (fun x -> (global_has_name (fst x))) symbols))
- with Not_found -> find_in_scope x Program)
- | Formal kf -> List.find_opt has_name (get_formals kf)
- | Whole_function kf -> List.find_opt has_name (get_locals kf)
+ let symbols,_ = List.split (FileIndex.get_globals file) in
+ List.find_opt global_has_name symbols |> lookup Program
+ | Formal kf ->
+ let file = (fst (get_location kf)).Filepath.pos_path in
+ List.find_opt has_name (get_formals kf) |>
+ lookup (Translation_unit file)
+ | Whole_function kf ->
+ List.find_opt has_name (get_locals kf @ !get_statics kf) |>
+ lookup (Formal kf)
| Block_scope stmt ->
let blocks = !find_all_enclosing_blocks stmt in
let find_in_block b =
@@ -697,17 +709,19 @@ module Syntactic_search = struct
raise (M.Found (List.find has_name b.bstatics))
in
try
- List.iter find_in_block blocks;
- let kf = !find_englobing_kf stmt in
- let filename = (fst ( get_location kf)).Filepath.pos_path in
- let formals = get_formals kf in
- if List.exists has_name formals then
- Some (List.find has_name formals)
+ (* blocks can't be empty, we have at least the body of the function. *)
+ find_in_block (List.hd blocks);
+ if strict then None
else
- find_in_scope x (Translation_unit filename)
+ begin
+ List.iter find_in_block (List.tl blocks);
+ let kf = !find_englobing_kf stmt in
+ if strict then None else find_in_scope x (Formal kf)
+ end
with M.Found v -> Some v
- and find_in_scope x scope = Scope_info.memo find_var (x,scope)
+ and find_in_scope ?(strict=false) x scope =
+ Scope_info.memo find_var (x,scope,strict)
end
diff --git a/src/kernel_services/ast_data/globals.mli b/src/kernel_services/ast_data/globals.mli
index 1a92f063c82a497235235aab05bf3cf24cc7b5b2..25bee52270650f758d6d725d0d224c316ed9cf4a 100644
--- a/src/kernel_services/ast_data/globals.mli
+++ b/src/kernel_services/ast_data/globals.mli
@@ -221,13 +221,24 @@ end
module Syntactic_search: sig
val self: State.t
- val find_in_scope: string -> syntactic_scope -> varinfo option
+ val find_in_scope: ?strict:bool -> string -> syntactic_scope -> varinfo option
(** [find_in_scope orig_name scope] finds a variable from its [orig_name],
according to the syntactic [scope] in which it should be searched.
+ @param strict indicates whether the symbol should be searched only in
+ the exact [scope] that it is given. It defaults to [false], meaning
+ that the search will look for enclosing scopes, according to C lookup
+ rules. More precisely, non-strict lookup will proceed according to the
+ following order: [Block_scope] will move across all enclosing blocks
+ up to the function body (or all locals will be searched directly in
+ case of [Whole_function]). Then, [Formal] will be considered, followed
+ by [Translation_unit] (for the file where the function is defined),
+ then [Program].
@return [None] if there are no variables [orig_name] in [scope].
@return [Some vi] otherwise, with [vi] the [varinfo] associated to
- [orig_name] in [scope] according to C lookup rules.
+ [orig_name] in [scope] (or an enclosing scope when [strict] is false).
@since Chlorine-20180501
+ @before Frama-C+dev [strict] parameter did not exist, symbol was always
+ searched according to C lookup rules.
*)
end
@@ -338,6 +349,7 @@ val get_comments_stmt: stmt -> string list
(* Forward reference to functions defined in Kernel_function. Do not
use outside of this module.
*)
+val get_statics: (kernel_function -> varinfo list) ref
val find_first_stmt: (kernel_function -> stmt) ref
val find_enclosing_block: (stmt -> block) ref
val find_all_enclosing_blocks: (stmt -> block list) ref
diff --git a/src/kernel_services/ast_data/kernel_function.ml b/src/kernel_services/ast_data/kernel_function.ml
index be29ec2b73fb94bc4a0bbdb433efd413e7d7e80f..1776d39211ec7d2ca18590947e62c903d807ce6f 100644
--- a/src/kernel_services/ast_data/kernel_function.ml
+++ b/src/kernel_services/ast_data/kernel_function.ml
@@ -67,6 +67,8 @@ let get_statics f = match f.fundec with
!statics
| Declaration (_, _, _, _) -> []
+let () = Globals.get_statics := get_statics
+
exception No_Definition
let get_definition kf = match kf.fundec with
| Definition (f,_) -> f
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index 98b9262539e6acc7659b135b28077a43dadcae30..919b0cc253acadb481fc44a9495fe281ec351663 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -580,7 +580,7 @@ let memo_aux_variable tr counter used_prms vi =
let check_one top info counter s =
match info with
| ECall (kf,used_prms,tr) ->
- Globals.Syntactic_search.find_in_scope s (Formal kf) |>
+ Globals.Syntactic_search.find_in_scope ~strict:true s (Formal kf) |>
(Fun.flip Option.bind
(fun vi ->
if top then Some (Logic_const.tvar (Cil.cvar_to_lvar vi))
@@ -669,7 +669,9 @@ let find_prm_in_env env ?tr counter f x =
(TCall (kf,None))
in
let vi =
- match Globals.Syntactic_search.find_in_scope x (Formal kf) with
+ match
+ Globals.Syntactic_search.find_in_scope ~strict:true x (Formal kf)
+ with
| Some vi -> vi
| None -> Aorai_option.abort "Function %s has no parameter %s" f x
in