diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index cccda3a9169be72d7c7d2202aec9827b2b477ada..8725e512b03f735eefc3107947a1c8d22ea29b51 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -841,6 +841,21 @@ let env : (string, envdata * location) H.t = H.create 307
(* We also keep a global environment. This is always a subset of the env *)
let genv : (string, envdata * location) H.t = H.create 307
+let label_env = Datatype.String.Hashtbl.create 307
+
+let add_label_env lab =
+ let add_if_absent v (d,_) map =
+ match d with
+ | EnvVar vi when not (Datatype.String.Map.mem v map) ->
+ Datatype.String.Map.add v vi map
+ | _ -> map
+ in
+ let lab_env = H.fold add_if_absent env Datatype.String.Map.empty in
+ Datatype.String.Hashtbl.add label_env lab lab_env
+
+let remove_label_env lab =
+ Datatype.String.Hashtbl.remove label_env lab
+
(* In the scope we keep the original name, so we can remove them from the
* hash table easily *)
type undoScope =
@@ -1021,6 +1036,7 @@ let constrExprId = ref 0
let startFile () =
+ Datatype.String.Hashtbl.clear label_env;
H.clear env;
H.clear genv;
H.clear alphaTable;
@@ -3719,9 +3735,27 @@ struct
let anonCompFieldName = anonCompFieldName
let conditionalConversion = logicConditionalConversion
let find_macro _ = raise Not_found
- let find_var x = match H.find env x with
- | EnvVar vi, _ -> cvar_to_lvar vi
- | _ -> raise Not_found
+ let find_var ?label ~var =
+ let find_from_curr_env test =
+ match H.find env var with
+ | EnvVar vi, _ when test vi -> cvar_to_lvar vi
+ | _ -> raise Not_found
+ in
+ match label with
+ | None -> find_from_curr_env (fun _ -> true)
+ | Some "Here" | Some "Old" | Some "Post" ->
+ (* the last two labels can only be found in contracts and refer
+ to the pre/post state of the contracts: all local variables
+ in scope at current point are also in scope in the labels. *)
+ find_from_curr_env (fun _ -> true)
+ | Some "Pre" ->
+ find_from_curr_env (fun vi -> vi.vformal || vi.vglob)
+ | Some "Init" -> find_from_curr_env (fun vi -> vi.vglob)
+ | Some lab ->
+ cvar_to_lvar
+ (Datatype.String.Map.find var
+ (Datatype.String.Hashtbl.find label_env lab))
+
let find_enum_tag x = match H.find env x with
| EnvEnum item,_ ->
dummy_exp (Const (CEnum item)), typeOf item.eival
@@ -3764,6 +3798,8 @@ module Ltyping = Logic_typing.Make (C_logic_env)
let startLoop iswhile =
incr C_logic_env.nb_loop;
+ add_label_env "LoopEntry";
+ add_label_env "LoopCurrent";
continues :=
(if iswhile then While (ref "") else NotWhile (ref "")) :: !continues;
enter_break_env ()
@@ -3771,6 +3807,8 @@ let startLoop iswhile =
let exitLoop () =
decr C_logic_env.nb_loop;
exit_break_env ();
+ remove_label_env "LoopEntry";
+ remove_label_env "LoopCurrent";
match !continues with
| [] -> Kernel.error ~once:true ~current:true "exit Loop not in a loop"
| _ :: rest -> continues := rest
@@ -9663,6 +9701,7 @@ and doStatement local_env (s : A.statement) : chunk =
| A.LABEL (l, s, loc) ->
let loc' = convLoc loc in
CurrentLoc.set loc';
+ add_label_env l;
C_logic_env.add_current_label l;
(* Lookup the label because it might have been locally defined *)
let chunk =
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 918ca0447b734454367bde0b04082b03bec3ff96..b0e2522c5bc025fbef5ad04970bb1257b2d2d8dc 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -326,6 +326,26 @@ module Lenv = struct
*)
}
+ let string_of_current_label env =
+ Extlib.opt_bind (
+ function
+ | FormalLabel _ -> None
+ | BuiltinLabel Init -> Some "Init"
+ | BuiltinLabel Pre -> Some "Pre"
+ | BuiltinLabel Old -> Some "Old"
+ | BuiltinLabel Post -> Some "Post"
+ | BuiltinLabel Here -> Some "Here"
+ | BuiltinLabel LoopCurrent -> Some "LoopCurrent"
+ | BuiltinLabel LoopEntry -> Some "LoopEntry"
+ | StmtLabel s ->
+ (match
+ List.find_opt (function Label (_,_,b) -> b | _ -> false) !s.labels
+ with
+ | None -> None
+ | Some (Label (lab,_,_)) -> Some lab
+ | Some _ -> None))
+ env.current_logic_label
+
let fresh_var env name kind typ =
let name =
let exists name =
@@ -468,7 +488,7 @@ type typing_context = {
anonCompFieldName : string;
conditionalConversion : typ -> typ -> typ;
find_macro : string -> lexpr;
- find_var : string -> logic_var;
+ find_var : ?label:string -> var:string -> logic_var;
find_enum_tag : string -> exp * typ;
find_comp_field: compinfo -> string -> offset;
find_type : type_namespace -> string -> typ;
@@ -633,7 +653,7 @@ module Make
val anonCompFieldName : string
val conditionalConversion : typ -> typ -> typ
val find_macro : string -> lexpr
- val find_var : string -> logic_var
+ val find_var : ?label:string -> var:string -> logic_var
val find_enum_tag : string -> exp * typ
val find_comp_field: compinfo -> string -> offset
val find_type : type_namespace -> string -> typ
@@ -2512,7 +2532,8 @@ struct
| _ -> old_val lv)
with Not_found ->
try
- let info = ctxt.find_var x in
+ let label = Lenv.string_of_current_label env in
+ let info = ctxt.find_var ?label ~var:x in
(match info.lv_origin with
| Some lv ->
check_current_label loc env;
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index a05bd2a0ebba3432098286cae6c3596702b3463c..11a48ce5cd5009fda29cba4d40cfbf4a8aa824c3 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -97,7 +97,11 @@ type typing_context = {
anonCompFieldName : string;
conditionalConversion : typ -> typ -> typ;
find_macro : string -> Logic_ptree.lexpr;
- find_var : string -> logic_var;
+ find_var : ?label:string -> var:string -> logic_var;
+ (** the label argument is a C label (obeying the restrictions
+ of which label can be present in a \at). If present, the scope for
+ searching local C variables is the one of the statement with
+ the corresponding label. *)
find_enum_tag : string -> exp * typ;
find_comp_field: compinfo -> string -> offset;
find_type : type_namespace -> string -> typ;
@@ -245,7 +249,8 @@ module Make
val anonCompFieldName : string
val conditionalConversion : typ -> typ -> typ
val find_macro : string -> Logic_ptree.lexpr
- val find_var : string -> logic_var
+ val find_var : ?label:string -> var:string -> logic_var
+ (** see corresponding field in {!Logic_typing.typing_context}. *)
val find_enum_tag : string -> exp * typ
val find_type : type_namespace -> string -> typ
val find_comp_field: compinfo -> string -> offset
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index b2933c2f6e1ffc0be435368090607402e25e9095..f5faca352f87dd495392aca4076b3f42c1f17b8d 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -652,7 +652,7 @@ struct
let conditionalConversion = Cabs2cil.logicConditionalConversion
let is_loop () = false
let find_macro _ = raise Not_found
- let find_var _ = raise Not_found
+ let find_var ?label:_ ~var:_ = raise Not_found
let find_enum_tag _ = raise Not_found
(*let find_comp_type ~kind:_ _ = raise Not_found*)
let find_comp_field info s =