diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 845919d8d1d0f03e82e61fb3fcc0d2d8fc5f221a..eb3177307c5d71e8f9037b17f89cb6f1e121fded 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;
@@ -1503,13 +1519,13 @@ struct
try
ref (H.find labels s)
with Not_found when List.mem s !label_current ->
- let my_ref =
- ref
- (mkEmptyStmt
- (* just a placeholder that will never be used. no need to
- check for ghost status here. *)
- ~ghost:false ~valid_sid ~loc:(cabslu "_find_label") ())
+ (* just a placeholder that will never be used. no need to
+ check for ghost status here. *)
+ let my_stmt =
+ mkEmptyStmt ~ghost:false ~valid_sid ~loc:(cabslu "_find_label") ()
in
+ my_stmt.labels <- [Label(s,cabslu "_find_label",true)];
+ let my_ref = ref my_stmt in
addGoto s my_ref; my_ref
end
@@ -3725,9 +3741,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
@@ -3770,6 +3804,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 ()
@@ -3777,6 +3813,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
@@ -9669,6 +9707,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/analysis/logic_interp.ml b/src/kernel_services/analysis/logic_interp.ml
index 8a82bb7009c44cdb18b0358052dc123bf79527ad..e8af8bc2a58e2fde1a50c2f14031a506b46a3388 100644
--- a/src/kernel_services/analysis/logic_interp.ml
+++ b/src/kernel_services/analysis/logic_interp.ml
@@ -27,14 +27,43 @@ open Cil_datatype
exception Error of Cil_types.location * string
exception Unbound of string
-let find_var kf x =
+let find_var kf kinstr ?label ~var =
let vi =
- try Globals.Vars.find_from_astinfo x (VLocal kf)
+ 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
+ | 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
+ | Some l ->
+ (try let s = Kernel_function.find_label kf l in !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)
with Not_found ->
try
- Globals.Vars.find_from_astinfo x (VFormal kf)
+ Globals.Vars.find_from_astinfo var (VFormal kf)
with Not_found ->
- Globals.Vars.find_from_astinfo x VGlobal
+ Globals.Vars.find_from_astinfo var VGlobal
in
cvar_to_lvar vi
@@ -46,18 +75,21 @@ let find_var kf x =
module DefaultLT (X:
sig
val kf: Kernel_function.t
- val in_loop: bool (* Only useful for code annotations *)
+ val kinstr: Cil_types.kinstr
end) =
Logic_typing.Make
(struct
let anonCompFieldName = Cabs2cil.anonCompFieldName
let conditionalConversion = Cabs2cil.logicConditionalConversion
- let is_loop () = X.in_loop
+ let is_loop () =
+ match X.kinstr with
+ | Kglobal -> false
+ | Kstmt s -> Kernel_function.stmt_in_loop X.kf s
let find_macro _ = raise Not_found
- let find_var x = find_var X.kf x
+ let find_var ?label ~var = find_var X.kf X.kinstr ?label ~var
let find_enum_tag x =
try
@@ -118,7 +150,7 @@ let code_annot kf stmt s =
sync_typedefs ();
let module LT = DefaultLT(struct
let kf = kf
- let in_loop = Kernel_function.stmt_in_loop kf stmt
+ let kinstr = Kstmt stmt
end) in
let loc = Stmt.loc stmt in
let pa =
@@ -141,7 +173,7 @@ let term kf ?(loc=Location.unknown) ?(env=default_term_env ()) s =
sync_typedefs ();
let module LT = DefaultLT(struct
let kf = kf
- let in_loop = false (* unused *)
+ let kinstr = Kglobal
end) in
let pa_expr = Extlib.opt_map snd (Logic_lexer.lexpr (fst loc, s)) in
let parse pa_expr = LT.term env pa_expr in
@@ -156,7 +188,7 @@ let predicate kf ?(loc=Location.unknown) ?(env=default_term_env ()) s =
sync_typedefs ();
let module LT = DefaultLT(struct
let kf = kf
- let in_loop = false (* unused *)
+ let kinstr = Kglobal
end) in
let pa_expr = Extlib.opt_map snd (Logic_lexer.lexpr (fst loc, s)) in
let parse pa_expr = LT.predicate env pa_expr in
diff --git a/src/kernel_services/ast_data/kernel_function.ml b/src/kernel_services/ast_data/kernel_function.ml
index 1d7d7d982b0cda0c31270cbb7c6692eb9d426f48..8e876e4d23bfee17053055c823884a4565903dd8 100644
--- a/src/kernel_services/ast_data/kernel_function.ml
+++ b/src/kernel_services/ast_data/kernel_function.ml
@@ -425,6 +425,12 @@ let find_syntactic_callsites kf =
try CallSites.find table kf
with Not_found -> []
+let var_is_in_scope stmt vi =
+ let blocks = find_all_enclosing_blocks stmt in
+ List.exists
+ (fun b -> List.exists (Cil_datatype.Varinfo.equal vi) b.blocals)
+ blocks
+
(* ************************************************************************* *)
(** {2 Checkers} *)
(* ************************************************************************* *)
diff --git a/src/kernel_services/ast_data/kernel_function.mli b/src/kernel_services/ast_data/kernel_function.mli
index d6700783c495fe773ecb3fc9af317b1732058340..18c1dac1287a83abf9be394c92e837802c8c22c9 100644
--- a/src/kernel_services/ast_data/kernel_function.mli
+++ b/src/kernel_services/ast_data/kernel_function.mli
@@ -127,6 +127,14 @@ val find_syntactic_callsites : t -> (t * stmt) list
[stmt].
@since Carbon-20110201 *)
+val var_is_in_scope: stmt -> varinfo -> bool
+ (** [var_is_in_scope kf stmt vi] returns [true] iff the local variable [vi]
+ is syntactically visible from statement [stmt] in function [kf]. Note
+ that on the contrary to {!Globals.Syntactic_search.find_in_scope}, the
+ variable is searched according to its [vid], not its [vorig_name].
+
+ @since Frama-C+dev *)
+
(* ************************************************************************* *)
(** {2 Checkers} *)
(* ************************************************************************* *)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 3696935c9266797f8316aa6d5b0fedc9d83bedd0..a5a205947e2da1f126523a65eacaee1c753ddcef 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -326,6 +326,27 @@ 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
+ Transitioning.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 +489,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 +654,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 +2533,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 c204d9df8e233d2970b951de6848ad4b04e0c0eb..eed2c7af32cd78be27c16b78726f20f7543bb883 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;
@@ -246,7 +250,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 =
diff --git a/tests/spec/at.c b/tests/spec/at.c
index b18cc464836c8badd181b0f7591e6a0dcc26c74b..9be4a3153ebb6356c671010287cb6bc457da0f95 100644
--- a/tests/spec/at.c
+++ b/tests/spec/at.c
@@ -22,6 +22,35 @@ int f(int y) {
return x;
}
+void test () {
+ int x = 0;
+ L1: {
+ int x = 1;
+ L2:
+ // assert below speaks about two distinct x.
+ /*@ assert \at(&x, L1) != \at(&x,L2); */
+ x = 2;
+ }
+}
+
+void ko (int z) {
+ L: {
+ int y = 0;
+ // assert below should not typecheck: y is not in scope at L (nor at Pre)
+ //@ assert KO: \at(y,L) == 0;
+ //@ assert KO: \at(y,Pre) == 0;
+ //@ assert KO: \at(z,Init) == 0; // at Init, only globals are in scope
+ //@ assert OK: \at (x,Init) == 0;
+ //@ assert OK: \at(z,Pre) == 0;
+ }
+ while (x>0) {
+ int i = 1;
+ x--;
+ //@ assert KO: \at(i,LoopCurrent) == 1;
+ //@ assert OK: \at(z,LoopCurrent) == \at(z,Pre);
+ }
+}
+
/*
Local Variables:
compile-command: "PPCHOME=../.. LC_ALL=C make at"
diff --git a/tests/spec/oracle/at.res.oracle b/tests/spec/oracle/at.res.oracle
index 31284982e1e899a3ff33e9be9367f392707e2676..8194269ad908387250693fe8d3d6a20f7d49b366 100644
--- a/tests/spec/oracle/at.res.oracle
+++ b/tests/spec/oracle/at.res.oracle
@@ -1,4 +1,12 @@
[kernel] Parsing tests/spec/at.c (with preprocessing)
+[kernel:annot-error] tests/spec/at.c:40: Warning:
+ unbound logic variable y. Ignoring code annotation
+[kernel:annot-error] tests/spec/at.c:41: Warning:
+ unbound logic variable y. Ignoring code annotation
+[kernel:annot-error] tests/spec/at.c:42: Warning:
+ unbound logic variable z. Ignoring code annotation
+[kernel:annot-error] tests/spec/at.c:49: Warning:
+ unbound logic variable i. Ignoring code annotation
/* Generated by Frama-C */
int x;
/*@
@@ -28,4 +36,32 @@ int f(int y)
return x;
}
+void test(void)
+{
+ int x_0 = 0;
+ L1:
+ {
+ int x_1 = 1;
+ L2: /*@ assert \at(&x_0,L1) ≢ \at(&x_1,L2); */ ;
+ x_1 = 2;
+ }
+ return;
+}
+
+void ko(int z)
+{
+ L:
+ {
+ int y = 0;
+ /*@ assert OK: \at(x,Init) ≡ 0; */ ;
+ /*@ assert OK: \at(z,Pre) ≡ 0; */ ;
+ }
+ while (x > 0) {
+ int i = 1;
+ x --;
+ /*@ assert OK: \at(z,LoopCurrent) ≡ \at(z,Pre); */ ;
+ }
+ return;
+}
+