Skip to content
Snippets Groups Projects
Commit eefaa2c0 authored by Thibault Martin's avatar Thibault Martin Committed by Virgile Prevosto
Browse files

[kernel] Var is in scope if sdef == stmt

parent 9b89de8b
No related branches found
No related tags found
No related merge requests found
...@@ -540,6 +540,8 @@ let var_is_in_scope stmt vi = ...@@ -540,6 +540,8 @@ let var_is_in_scope stmt vi =
let blocks = find_all_enclosing_blocks stmt in let blocks = find_all_enclosing_blocks stmt in
let is_def_above b = let is_def_above b =
let sdef = local_definition (find_englobing_kf stmt) vi in let sdef = local_definition (find_englobing_kf stmt) vi in
(* If sdef == stmt, vi is in the scope. *)
Cil_datatype.Stmt.equal sdef stmt ||
match b.bstmts with match b.bstmts with
| [] -> assert false (* at least contains stmt *) | [] -> assert false (* at least contains stmt *)
| sfst :: _ -> | sfst :: _ ->
......
...@@ -143,7 +143,7 @@ val local_definition: t -> varinfo -> stmt ...@@ -143,7 +143,7 @@ val local_definition: t -> varinfo -> stmt
*) *)
val var_is_in_scope: stmt -> varinfo -> bool val var_is_in_scope: stmt -> varinfo -> bool
(** [var_is_in_scope kf stmt vi] returns [true] iff the local variable [vi] (** [var_is_in_scope stmt vi] returns [true] iff the local variable [vi]
is syntactically visible from statement [stmt] in function [kf]. Note is syntactically visible from statement [stmt] in function [kf]. Note
that on the contrary to {!Globals.Syntactic_search.find_in_scope}, the that on the contrary to {!Globals.Syntactic_search.find_in_scope}, the
variable is searched according to its [vid], not its [vorig_name]. variable is searched according to its [vid], not its [vorig_name].
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment