diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index 21a599460d2fdb73bd81e6e805e3c075424be978..ae2431695307561dd157c601799117b5f6650c4f 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -1836,27 +1836,31 @@ type kernel_function = {
mutable spec : funspec;
}
-(* [VP] TODO: VLocal should be attached to a particular block, not a whole
- function. It might be worth it to unify this type with the newer
- syntactic_scope below.
-*)
-type localisation =
- | VGlobal
- | VLocal of kernel_function
- | VFormal of kernel_function
-
(** Various syntactic scopes through which an identifier might be searched.
Note that for this purpose static variables are still tied to the block
where they were declared in the original source (see {!Cil_types.block}).
@since Chlorine-20180501
*)
type syntactic_scope =
+ | Global
+ (** Any global symbol, whether static or not.
+ @since Frama-C+dev
+ *)
| Program (** Only non-static global symbols. *)
| Translation_unit of Filepath.Normalized.t
(** Any global visible within the given C source file. *)
+ | Formal of kernel_function
+ (** formal parameter of the given function.
+ @since Frama-C+dev
+ *)
| Block_scope of stmt
- (** same as above + all locals of the blocks to which the given statement
+ (** globals + all locals of the blocks to which the given statement
belongs. *)
+ | Whole_function of kernel_function
+ (** same as above, but any local variable of the given function, regardless of
+ the block to which it is tied, will be considered.
+ @since Frama-C+dev
+ *)
(** Definition of a machine model (architecture + compiler).
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
diff --git a/src/kernel_services/ast_data/globals.ml b/src/kernel_services/ast_data/globals.ml
index 42b251943f4224c468d6d214c88d10aa91f1dcd4..979aed0a1fe46383ac61c6f41fac5a2f76f24732 100644
--- a/src/kernel_services/ast_data/globals.ml
+++ b/src/kernel_services/ast_data/globals.ml
@@ -73,21 +73,40 @@ module Vars = struct
let add_decl vi = add vi { init = None }
- let get_astinfo_ref : (Cil_types.varinfo -> string * localisation) ref =
+ let get_astinfo_ref : (Cil_types.varinfo -> string * syntactic_scope) ref =
Extlib.mk_fun "get_astinfo_ref"
exception Found of varinfo
- let find_from_astinfo name = function
- | VGlobal ->
- (try
- iter (fun v _ -> if v.vname = name then raise (Found v));
- raise Not_found
- with Found v ->
- v)
- | VLocal kf ->
+ let find_from_astinfo name scope =
+ let iter_glob cond =
+ try
+ iter (fun v _ -> if cond v then raise (Found v));
+ raise Not_found
+ with Found v -> v
+ in
+ match scope with
+ | Global -> iter_glob (fun v -> v.vname = name)
+ | Program ->
+ iter_glob (fun v -> v.vname = name && not (v.vstorage = Static))
+ | Translation_unit file ->
+ iter_glob
+ (fun v ->
+ 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)
- | VFormal kf ->
+ | Formal kf ->
List.find (fun v -> v.vname = name) (get_formals kf)
+ | Block_scope stmt ->
+ let blocks = !find_all_enclosing_blocks stmt in
+ (try
+ List.iter
+ (fun b ->
+ (List.iter (fun v -> if v.vname = name then raise (Found v))
+ (b.blocals @ b.bstatics)))
+ blocks;
+ raise Not_found
+ with Found v -> v)
let get_astinfo vi = !get_astinfo_ref vi
@@ -394,7 +413,12 @@ module Functions = struct
exception Found of kernel_function
let get_astinfo vi =
vi.vname,
- if vi.vglob then VGlobal
+ if vi.vglob then begin
+ if vi.vstorage = Static then
+ Translation_unit (fst vi.vdecl).pos_path
+ else
+ Program
+ end
else begin
if vi.vformal then begin
try
@@ -404,7 +428,7 @@ module Functions = struct
then raise (Found kf));
assert false
with Found kf ->
- VFormal kf
+ Formal kf
end else begin
try
iter
@@ -413,7 +437,8 @@ module Functions = struct
then raise (Found kf));
assert false
with Found kf ->
- VLocal kf
+ (* TODO: find the block where the varinfo is defined. *)
+ Whole_function kf
end
end
@@ -647,6 +672,11 @@ module Syntactic_search = struct
in
let module M = struct exception Found of varinfo end in
match scope with
+ | Global ->
+ (try
+ Vars.iter (fun v _ -> if has_name v then raise (M.Found v));
+ None
+ with M.Found v -> Some v)
| Program ->
(try
Vars.iter (fun v _ -> if global_has_name v then raise (M.Found v));
@@ -656,6 +686,8 @@ module Syntactic_search = struct
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)
| Block_scope stmt ->
let blocks = !find_all_enclosing_blocks stmt in
let find_in_block b =
diff --git a/src/kernel_services/ast_data/globals.mli b/src/kernel_services/ast_data/globals.mli
index 51ff3e98930da8c361f16d549623fce442cbbc93..1a92f063c82a497235235aab05bf3cf24cc7b5b2 100644
--- a/src/kernel_services/ast_data/globals.mli
+++ b/src/kernel_services/ast_data/globals.mli
@@ -35,7 +35,7 @@ module Vars: sig
val find: varinfo -> initinfo
- val find_from_astinfo: string -> localisation -> varinfo
+ val find_from_astinfo: string -> syntactic_scope -> varinfo
(** Finds a variable from its [vname] according to its localisation (which
might be a local). If you wish to search for a symbol according to its
original name in the source code and the syntactic scope in which
@@ -43,7 +43,7 @@ module Vars: sig
@raise Not_found if no such variable exists.
*)
- val get_astinfo: varinfo -> string * localisation
+ val get_astinfo: varinfo -> string * syntactic_scope
(** Linear in the number of locals and formals of the program. *)
(** {2 Iterators} *)
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index 052943406bf0f43ed5cde2c2c43c2cbb2e5e632c..b0969a74015cd5d260209ffa97a2687d43333ff7 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -1035,10 +1035,15 @@ let pp_kernel_function fmt kernel_function =
pp_cil_function kernel_function.fundec
pp_funspec kernel_function.spec
-let pp_localisation fmt = function
- | VGlobal -> Format.fprintf fmt "VGlobal"
- | VLocal(kernel_function) -> Format.fprintf fmt "VLocal(%a)" pp_kernel_function kernel_function
- | VFormal(kernel_function) -> Format.fprintf fmt "VFormal(%a)" pp_kernel_function kernel_function
+let pp_syntactic_scope fmt = function
+ | Global -> pp_string fmt "Global"
+ | Program -> pp_string fmt "Program"
+ | Translation_unit file ->
+ Format.fprintf fmt "Translation_unit %S" (file:>string)
+ | Formal kf -> Format.fprintf fmt "Formal %a" pp_kernel_function kf
+ | Block_scope stmt -> Format.fprintf fmt "Local %a" pp_stmt stmt
+ | Whole_function kf ->
+ Format.fprintf fmt "Whole_function %a" pp_kernel_function kf
let pp_mach fmt mach =
Format.fprintf fmt
diff --git a/src/kernel_services/ast_printing/cil_types_debug.mli b/src/kernel_services/ast_printing/cil_types_debug.mli
index cf447e2ad48636736196b54fe87b81f6bb754aef..e9d3c6fb74aa75dd700d3ed7812ad0406449817a 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.mli
+++ b/src/kernel_services/ast_printing/cil_types_debug.mli
@@ -157,5 +157,5 @@ val pp_global_annotation : Cil_types.global_annotation Pretty_utils.formatter
val pp_kinstr : Format.formatter -> Cil_types.kinstr -> unit
val pp_cil_function : Format.formatter -> Cil_types.cil_function -> unit
val pp_kernel_function : Format.formatter -> Cil_types.kernel_function -> unit
-val pp_localisation : Format.formatter -> Cil_types.localisation -> unit
+val pp_syntactic_scope: Format.formatter -> Cil_types.syntactic_scope -> unit
val pp_mach : Format.formatter -> Cil_types.mach -> unit
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index de58f03133ae3fbc11682cd552b454bbed0b12ec..222d4c77a26e2b10ba247b08b698d63ff7a6b886 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -1388,7 +1388,7 @@ and enumitem_correspondence ?loc ei env =
and gvar_correspondence ?loc vi env =
let add vi =
- match find_candidate_varinfo ?loc vi Cil_types.VGlobal with
+ match find_candidate_varinfo ?loc vi Cil_types.Global with
| None when Cil.isFunctionType vi.vtype ->
begin
match gfun_correspondence ?loc vi env with
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 25c688a55d5671f268e68b266802a810db6ff9dc..d08d58bc8b1aeaf61d6b1364621e54c2a1122f45 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -2579,16 +2579,6 @@ module Lexpr = Make
(** {3 Other types} *)
(**************************************************************************)
-module Localisation =
- Datatype.Make
- (struct
- include Datatype.Serializable_undefined
- type t = localisation
- let name = "Localisation"
- let reprs = [ VGlobal ]
- let mem_project = Datatype.never_any_project
- end)
-
module Syntactic_scope =
Datatype.Make_with_collections
(struct
@@ -2598,6 +2588,9 @@ module Syntactic_scope =
let reprs = [ Program ]
let compare s1 s2 =
match s1, s2 with
+ | Global, Global -> 0
+ | Global, _ -> 1
+ | _, Global -> -1
| Program, Program -> 0
| Program, _ -> 1
| _, Program -> -1
@@ -2605,17 +2598,30 @@ module Syntactic_scope =
Datatype.Filepath.compare s1 s2
| Translation_unit _, _ -> 1
| _, Translation_unit _ -> -1
+ | Formal kf1, Formal kf2 -> Kf.compare kf1 kf2
+ | Formal _, _ -> 1
+ | _, Formal _ -> -1
+ | Whole_function kf1, Whole_function kf2 -> Kf.compare kf1 kf2
+ | Whole_function _, _ -> 1
+ | _, Whole_function _ -> -1
| Block_scope s1, Block_scope s2 -> Stmt_Id.compare s1 s2
let equal = Datatype.from_compare
let hash s =
match s with
+ | Global -> 3
| Program -> 5
| Translation_unit s -> 7 * Datatype.Filepath.hash s + 11
| Block_scope s -> 13 * Stmt_Id.hash s + 17
+ | Whole_function kf -> 19 * Kf.hash kf + 23
+ | Formal kf -> 29 * Kf.hash kf + 31
let pretty fmt = function
- | Program -> Format.pp_print_string fmt "<Whole Program>"
+ | Global | Program -> Format.pp_print_string fmt "<Whole Program>"
| Translation_unit s ->
Format.fprintf fmt "File %a" Datatype.Filepath.pretty s
+ | Formal kf ->
+ Format.fprintf fmt "Parameter of %a" Kf.pretty kf
+ | Whole_function kf ->
+ Format.fprintf fmt "Local variable of %a" Kf.pretty kf
| Block_scope s ->
Format.fprintf fmt "Statement at %a:@\n@[%a@]"
Location.pretty (Stmt.loc s) Stmt.pretty s
diff --git a/src/kernel_services/ast_queries/cil_datatype.mli b/src/kernel_services/ast_queries/cil_datatype.mli
index efdc0387d21f1e6ae9daa8bd46bc1ec8517ba195..de601cca4d4a3031b9b1b6ead68d4150b26d6d4c 100644
--- a/src/kernel_services/ast_queries/cil_datatype.mli
+++ b/src/kernel_services/ast_queries/cil_datatype.mli
@@ -102,8 +102,6 @@ module Location: sig
val equal_start_semantic : location -> location -> bool
end
-module Localisation: Datatype.S with type t = localisation
-
module Syntactic_scope:
Datatype.S_with_collections with type t = syntactic_scope
diff --git a/src/kernel_services/ast_queries/logic_parse_string.ml b/src/kernel_services/ast_queries/logic_parse_string.ml
index db62131f6e9554636d042c46fb1b5b86777468eb..a75626bd53c6f3927ca95be6d93e1c7e40faa12e 100644
--- a/src/kernel_services/ast_queries/logic_parse_string.ml
+++ b/src/kernel_services/ast_queries/logic_parse_string.ml
@@ -30,40 +30,32 @@ exception Unbound of string
let find_var kf kinstr ?label var =
let vi =
try
- let vi = Globals.Vars.find_from_astinfo var (VLocal kf) in
- (match kinstr with
- | Kglobal -> vi (* don't refine search: the Kglobal here
- does not indicate the function contract, but merely
- the fact that we do not have any information about
- the targeted program point. Hence, no scope check
- can be performed or we might reject many legitimate
- terms and predicates.
- *)
- | Kstmt stmt ->
- let scope =
- match label with
- | None | Some "Here" | Some "Post" | Some "Old" -> stmt
+ let scope =
+ match kinstr with
+ | Kglobal -> Whole_function kf
+ | Kstmt stmt ->
+ (match label with
+ | None | Some "Here" | Some "Post" | Some "Old" -> Block_scope stmt
| Some "Pre" -> raise Not_found (* no local variable in scope. *)
| Some "Init" -> raise Not_found (* no local variable in scope. *)
| Some "LoopEntry" | Some "LoopCurrent" ->
if not (Kernel_function.stmt_in_loop kf stmt) then
Kernel.fatal
"Use of LoopEntry or LoopCurrent outside of a loop";
- Kernel_function.find_enclosing_loop kf stmt
+ Block_scope (Kernel_function.find_enclosing_loop kf stmt)
| Some l ->
- (try let s = Kernel_function.find_label kf l in !s
+ (try let s = Kernel_function.find_label kf l in Block_scope !s
with Not_found ->
Kernel.fatal
"Use of label %s that does not exist in function %a"
- l Kernel_function.pretty kf)
- in
- if Kernel_function.var_is_in_scope scope vi then vi
- else raise Not_found)
+ l Kernel_function.pretty kf))
+ in
+ Globals.Vars.find_from_astinfo var scope
with Not_found ->
try
- Globals.Vars.find_from_astinfo var (VFormal kf)
+ Globals.Vars.find_from_astinfo var (Formal kf)
with Not_found ->
- Globals.Vars.find_from_astinfo var VGlobal
+ Globals.Vars.find_from_astinfo var Global
in
cvar_to_lvar vi
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index 48d444ca8669159db94d0f306afc591eda739207..23685c5dde7f246d2bc7d5a4e0e9a82308f19d3d 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -705,7 +705,7 @@ let mk_gvar ?init ~ty name =
let vi =
try
let ty' = typeAddAttributes [Attr ("ghost", [])] ty in
- let vi = Globals.Vars.find_from_astinfo name VGlobal in
+ let vi = Globals.Vars.find_from_astinfo name Global in
if not (Cil_datatype.Typ.equal vi.vtype ty') then
Aorai_option.abort "Global %s is declared with type %a instead of %a"
name Cil_printer.pp_typ vi.vtype Cil_printer.pp_typ ty';
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index 66b550bdf3ab31f64d1154bba8c9631e2907a01a..98b9262539e6acc7659b135b28077a43dadcae30 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -258,7 +258,7 @@ let getNumberOfStates () =
let is_c_global name =
- try ignore (Globals.Vars.find_from_astinfo name VGlobal); true
+ try ignore (Globals.Vars.find_from_astinfo name Global); true
with Not_found ->
try ignore (Globals.Functions.find_by_name name); true
with Not_found -> false
@@ -580,11 +580,11 @@ let memo_aux_variable tr counter used_prms vi =
let check_one top info counter s =
match info with
| ECall (kf,used_prms,tr) ->
- (try
- let vi = Globals.Vars.find_from_astinfo s (VFormal kf) in
- if top then Some (Logic_const.tvar (Cil.cvar_to_lvar vi))
- else Some (memo_aux_variable tr counter used_prms vi)
- with Not_found -> None)
+ Globals.Syntactic_search.find_in_scope s (Formal kf) |>
+ (Fun.flip Option.bind
+ (fun vi ->
+ if top then Some (Logic_const.tvar (Cil.cvar_to_lvar vi))
+ else Some (memo_aux_variable tr counter used_prms vi)))
| EReturn kf when top && ( Datatype.String.equal s "return"
|| Datatype.String.equal s "\\result") ->
let rt = Kernel_function.get_return_type kf in
@@ -619,11 +619,11 @@ let find_in_env env counter s =
None -> ()
| Some lv -> raise (M.Found lv))
stack;
- let vi = Globals.Vars.find_from_astinfo s VGlobal in
- Logic_const.tvar (Cil.cvar_to_lvar vi)
+ (match Globals.Syntactic_search.find_in_scope s Program with
+ | Some vi -> Logic_const.tvar (Cil.cvar_to_lvar vi)
+ | None -> Aorai_option.abort "Unknown variable %s" s)
with
- M.Found lv -> lv
- | Not_found -> Aorai_option.abort "Unknown variable %s" s)
+ M.Found lv -> lv)
let find_prm_in_env env ?tr counter f x =
let kf =
@@ -669,9 +669,9 @@ let find_prm_in_env env ?tr counter f x =
(TCall (kf,None))
in
let vi =
- try Globals.Vars.find_from_astinfo x (VFormal kf)
- with Not_found ->
- Aorai_option.abort "Function %s has no parameter %s" f x
+ match Globals.Syntactic_search.find_in_scope x (Formal kf) with
+ | Some vi -> vi
+ | None -> Aorai_option.abort "Function %s has no parameter %s" f x
in
(* By definition, we are at the call event: no need to store
it in an aux variable or array here.
diff --git a/src/plugins/dive/self.ml b/src/plugins/dive/self.ml
index 4e3bb2c1eef4774d191c2084ee7107b65cf29c20..df6cbfc9216ce23512ee8496d27abe6913b1116e 100644
--- a/src/plugins/dive/self.ml
+++ b/src/plugins/dive/self.ml
@@ -75,9 +75,9 @@ struct
with Not_found ->
raise (Cannot_build ("no function '" ^ function_name ^ "'"))
in
- try Globals.Vars.find_from_astinfo variable_name (VLocal kf)
+ try Globals.Vars.find_from_astinfo variable_name (Whole_function kf)
with Not_found ->
- try Globals.Vars.find_from_astinfo variable_name (VFormal kf)
+ try Globals.Vars.find_from_astinfo variable_name (Formal kf)
with Not_found ->
raise (Cannot_build ("no variable '" ^ variable_name ^ "' in function "
^ function_name))
diff --git a/src/plugins/eva/partitioning/partitioning_parameters.ml b/src/plugins/eva/partitioning/partitioning_parameters.ml
index f2ecaebbb2c88b0fa3e27a5e530fabc22e51d95f..bbea9b87aed55ef78df676d4cb53fb1d5ffdaa4e 100644
--- a/src/plugins/eva/partitioning/partitioning_parameters.ml
+++ b/src/plugins/eva/partitioning/partitioning_parameters.ml
@@ -109,7 +109,7 @@ struct
let universal_splits =
let add name l =
try
- let vi = Globals.Vars.find_from_astinfo name VGlobal in
+ let vi = Globals.Vars.find_from_astinfo name Global in
let monitor = Partition.new_monitor ~split_limit in
let expr = Partition.Expression (Cil.evar vi) in
Partition.Split (expr, Partition.Dynamic, monitor) :: l
diff --git a/src/plugins/impact/compute_impact.ml b/src/plugins/impact/compute_impact.ml
index 66da42c04b433b1daff3572074ee3a0c0a109373..6f78536af6a6deb3c7e433fab4d0ca57dc01c4f5 100644
--- a/src/plugins/impact/compute_impact.ml
+++ b/src/plugins/impact/compute_impact.ml
@@ -711,7 +711,7 @@ let skip () =
(fun name l ->
let vi =
try
- Base.of_varinfo (Globals.Vars.find_from_astinfo name VGlobal)
+ Base.of_varinfo (Globals.Vars.find_from_astinfo name Global)
with Not_found ->
if name = "NULL" then Base.null
else
diff --git a/src/plugins/instantiate/global_context.ml b/src/plugins/instantiate/global_context.ml
index 178fb6d0cb4afe7a79391442f4ea3c2c5e689f75..c48802ba74273d601e294059d137cdd30e98cb7e 100644
--- a/src/plugins/instantiate/global_context.ml
+++ b/src/plugins/instantiate/global_context.ml
@@ -29,7 +29,7 @@ let axiomatics = Table.create 13
let get_variable name make =
if Table.mem varinfos name then Table.find varinfos name
else begin
- try Globals.Vars.find_from_astinfo name VGlobal
+ try Globals.Vars.find_from_astinfo name Global
with Not_found ->
let vi = make () in
Table.add varinfos name vi ;
diff --git a/tests/misc/add_assigns.ml b/tests/misc/add_assigns.ml
index 11df28607ac8e92edffb3d1ef12b31e1b4f8440d..04d7bec1b147135f8b102a33365da9196a1c918f 100644
--- a/tests/misc/add_assigns.ml
+++ b/tests/misc/add_assigns.ml
@@ -11,7 +11,7 @@ let main () =
computed := true;
Ast.compute ();
let kf = Globals.Functions.find_by_name "f" in
- let y = Globals.Vars.find_from_astinfo "y" (VFormal kf) in
+ let y = Globals.Vars.find_from_astinfo "y" (Formal kf) in
let mem =
Logic_const.(
new_identified_term
diff --git a/tests/spec/property_test.ml b/tests/spec/property_test.ml
index 00407c161ac46f53abe7aa0ccd0f38fc3d5a203d..9088cf306802455e82893b4042ccd39921790e5c 100644
--- a/tests/spec/property_test.ml
+++ b/tests/spec/property_test.ml
@@ -10,9 +10,9 @@ class visit prj =
method! vbehavior b =
let kf = Option.get self#current_kf in
if Kernel_function.get_name kf = "main" then begin
- let x = Globals.Vars.find_from_astinfo "X" VGlobal in
+ let x = Globals.Vars.find_from_astinfo "X" Global in
let x = Cil.cvar_to_lvar x in
- let c = Globals.Vars.find_from_astinfo "c" (VFormal kf) in
+ let c = Globals.Vars.find_from_astinfo "c" (Formal kf) in
let c = Cil.cvar_to_lvar c in
b.b_assigns <-
Writes
diff --git a/tests/syntax/get_astinfo_bts1136.ml b/tests/syntax/get_astinfo_bts1136.ml
index 98c338bf7c935b57c284e2392d2380a4460982b8..e842f7e046d687f023eca1e6c8563c03d6d33ccf 100644
--- a/tests/syntax/get_astinfo_bts1136.ml
+++ b/tests/syntax/get_astinfo_bts1136.ml
@@ -2,7 +2,7 @@
let get_formal_variables name =
let add_kf_vars kf vars =
try
- let v = Globals.Vars.find_from_astinfo name (Cil_types.VFormal kf) in
+ let v = Globals.Vars.find_from_astinfo name (Cil_types.Formal kf) in
Format.printf "found variable vid:%d formal in %a@."
v.Cil_types.vid Cil_datatype.Kf.pretty kf;
v::vars
@@ -14,7 +14,8 @@ let get_formal_variables name =
let get_local_variables name =
let add_kf_vars kf vars =
try
- let v = Globals.Vars.find_from_astinfo name (Cil_types.VLocal kf) in
+ let v = Globals.Vars.find_from_astinfo name (Cil_types.Whole_function kf)
+ in
Format.printf "found variable vid:%d formal in %a@."
v.Cil_types.vid Cil_datatype.Kf.pretty kf;
v::vars
@@ -30,16 +31,9 @@ let main () =
let vars = get_formal_variables "x" in
let vars' = get_local_variables "y" in
let do_v v =
- let pp_kind fmt kind = match kind with
- | Cil_types.VGlobal -> Format.fprintf fmt "global"
- | Cil_types.VFormal kf ->
- Format.fprintf fmt "formal in %a" Cil_datatype.Kf.pretty kf
- | Cil_types.VLocal kf ->
- Format.fprintf fmt "local in %a" Cil_datatype.Kf.pretty kf
- in
let _, kind = Globals.Vars.get_astinfo v in
Format.printf "[do_v] vid:%d %a@." v.Cil_types.vid
- (* Cil_datatype.Localisation.pretty *) pp_kind kind
+ Cil_datatype.Syntactic_scope.pretty kind
in List.iter do_v vars; List.iter do_v vars'
let () = Db.Main.extend main
diff --git a/tests/syntax/oracle/get_astinfo_bts1136.res.oracle b/tests/syntax/oracle/get_astinfo_bts1136.res.oracle
index 4201820cc17bf86f68100ee87549a14636977e5d..9c4b065ef072af884ea981f90301358d6285755b 100644
--- a/tests/syntax/oracle/get_astinfo_bts1136.res.oracle
+++ b/tests/syntax/oracle/get_astinfo_bts1136.res.oracle
@@ -5,9 +5,9 @@ found variable vid:28 formal in h
found variable vid:30 formal in i
found variable vid:32 formal in j
found variable vid:34 formal in k
-[do_v] vid:28 formal in h
-[do_v] vid:25 formal in g
-[do_v] vid:22 formal in f
-[do_v] vid:34 local in k
-[do_v] vid:32 local in j
-[do_v] vid:30 local in i
+[do_v] vid:28 Parameter of h
+[do_v] vid:25 Parameter of g
+[do_v] vid:22 Parameter of f
+[do_v] vid:34 Local variable of k
+[do_v] vid:32 Local variable of j
+[do_v] vid:30 Local variable of i