From 384a6bbcc5ba8a41aa0b4a4ce76226f808693a89 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 30 Mar 2023 18:16:26 +0200
Subject: [PATCH] [kernel] Unify types for symbol lookup context
---
src/kernel_services/ast_data/cil_types.ml | 24 ++++----
src/kernel_services/ast_data/globals.ml | 58 ++++++++++++++-----
src/kernel_services/ast_data/globals.mli | 4 +-
.../ast_printing/cil_types_debug.ml | 13 +++--
.../ast_printing/cil_types_debug.mli | 2 +-
src/kernel_services/ast_queries/ast_diff.ml | 2 +-
.../ast_queries/cil_datatype.ml | 28 +++++----
.../ast_queries/cil_datatype.mli | 2 -
.../ast_queries/logic_parse_string.ml | 34 +++++------
src/plugins/aorai/aorai_utils.ml | 2 +-
src/plugins/aorai/data_for_aorai.ml | 26 ++++-----
src/plugins/dive/self.ml | 4 +-
.../partitioning/partitioning_parameters.ml | 2 +-
src/plugins/impact/compute_impact.ml | 2 +-
src/plugins/instantiate/global_context.ml | 2 +-
tests/misc/add_assigns.ml | 2 +-
tests/spec/property_test.ml | 4 +-
tests/syntax/get_astinfo_bts1136.ml | 14 ++---
.../oracle/get_astinfo_bts1136.res.oracle | 12 ++--
19 files changed, 134 insertions(+), 103 deletions(-)
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index 21a599460d2..ae243169530 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 42b251943f4..979aed0a1fe 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 51ff3e98930..1a92f063c82 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 052943406bf..b0969a74015 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 cf447e2ad48..e9d3c6fb74a 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 de58f03133a..222d4c77a26 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 25c688a55d5..d08d58bc8b1 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 efdc0387d21..de601cca4d4 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 db62131f6e9..a75626bd53c 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 48d444ca866..23685c5dde7 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 66b550bdf3a..98b9262539e 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 4e3bb2c1eef..df6cbfc9216 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 f2ecaebbb2c..bbea9b87aed 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 66da42c04b4..6f78536af6a 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 178fb6d0cb4..c48802ba742 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 11df28607ac..04d7bec1b14 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 00407c161ac..9088cf30680 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 98c338bf7c9..e842f7e046d 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 4201820cc17..9c4b065ef07 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
--
GitLab