diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 4bd3d232a6e0eecef3971e71c3970df8eff36300..27b87593005255d178966a2b90f98e9ffa9e667d 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -2749,7 +2749,7 @@ let makeGlobalVarinfo (isadef: bool) (vi: varinfo) : varinfo * bool =
prototypes. Logic specifications refer to the varinfo in this table. *)
begin
match vi.vtype with
- | TFun (_, Some formals , _, _) ->
+ | TFun (_,Some formals , _, _ ) ->
(try
let old_formals_env = getFormalsDecl oldvi in
List.iter2
@@ -2770,14 +2770,14 @@ let makeGlobalVarinfo (isadef: bool) (vi: varinfo) : varinfo * bool =
old.vattr <- attr;
end;
match old.vlogic_var_assoc with
- | None -> ()
+ | None -> ()
| Some old_lv -> old_lv.lv_name <- name
end)
old_formals_env
formals
with Not_found -> Cil.setFormalsDecl oldvi vi.vtype)
| _ -> ()
- end;
+ end ;
(* if [isadef] is true, [vi] is a definition. *)
if isadef then begin
(* always favor the location of the definition.*)
@@ -8592,15 +8592,15 @@ and createGlobal loc ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool
let<> UpdatedCurrentLoc = loc in
let loc = Current_loc.get () in
let res =
- try
- (* it can not have old behavior names, since this is the
- first time we see the declaration.
- *)
- Ltyping.funspec [] vi None vi.vtype spec
- with LogicTypeError ((source,_),msg) ->
- Kernel.warning ~wkey:Kernel.wkey_annot_error ~source
- "%s. Ignoring specification of function %s" msg vi.vname;
- empty_funspec ()
+ try
+ (* it can not have old behavior names, since this is the
+ first time we see the declaration.
+ *)
+ Ltyping.funspec [] vi None vi.vtype spec
+ with LogicTypeError ((source,_),msg) ->
+ Kernel.warning ~wkey:Kernel.wkey_annot_error ~source
+ "%s. Ignoring specification of function %s" msg vi.vname;
+ empty_funspec ()
in
res, loc
end
@@ -10052,6 +10052,17 @@ and doStatement local_env (s : Cabs.statement) : chunk =
defaultChunk ~ghost loc' (doStatement local_env s)
| Cabs.LABEL (l, s, loc) ->
let loc' = convLoc loc in
+ Option.iter
+ begin fun label ->
+ let context = match label with
+ | Here | Pre | Init -> "annotations"
+ | LoopEntry | LoopCurrent -> "loop annotations"
+ | Old | Post -> "contracts"
+ in
+ Kernel.warning ~current:true
+ "%s is a builtin ACSL label, this C label is hidden in %s" l context
+ end
+ (Logic_typing.builtin_label l) ;
add_label_env l;
C_logic_env.add_current_label l;
(* Lookup the label because it might have been locally defined *)
diff --git a/src/kernel_internals/typing/rmtmps.ml b/src/kernel_internals/typing/rmtmps.ml
index 87dffa91bc7a0a0061b6c6ac39eacb15b3e0da8f..58ea3289bda12d383ea0b566d614c43432c788fe 100644
--- a/src/kernel_internals/typing/rmtmps.ml
+++ b/src/kernel_internals/typing/rmtmps.ml
@@ -674,6 +674,52 @@ let markReferenced ast =
*
**********************************************************************)
+(* Assumption: one can order logic labels according to their visibility.
+
+ The goal of this function is to minimize name clash when the program contains
+ C labels with a name that correspond to a builtin logic label. Parsing the
+ result should not lead to a program with a different semantics.
+ For example: [Here: Old: ;]
+ cannot be normalized into: [Here: ;]
+ because it could change the semantics of: [//@ assert P{Old};]
+
+ The behavior is as follows:
+ - select a name without name clash if there is one,
+ - else, order preferencer by visibility: Post > Old > Loop* > Other
+
+ A difference in semantics can appear if:
+ - there are several builtin label names with different visibilities
+ - there is an assertion that uses one non-visible label from this list
+ - we select a visible label from the list
+
+ By selecting the less visible we guarantee that we do not change the
+ semantics: either the selected label was not visible, it is not more visible
+ now, or it was already visible and thus already masked during the typing
+ phase.
+*)
+
+let prefer ~new_label ~old_label =
+ old_label = "" ||
+ match Logic_typing.builtin_label old_label with
+ | None -> false (* the old label already has a good name *)
+ | Some l_over ->
+ match Logic_typing.builtin_label new_label with
+ | None -> true (* the old label is a builtin name, the new one is better *)
+ | Some l_label ->
+ (* Ok, from now, we only have choices that are not good :( let's try to
+ minimize name clashes ...
+ *)
+ match l_label, l_over with
+ (* only visible in function contracts *)
+ | Post, _ -> true | _, Post -> false
+ (* only visible in contracts *)
+ | Old, _ -> true | _, Old -> false
+ (* only visible in annotations associated to a loop *)
+ | (LoopCurrent | LoopEntry), _ -> true
+ | _, (LoopCurrent | LoopEntry) -> false
+ (* ok, now we give up: anything else is visible in code annotations *)
+ | _ -> false
+
(* We keep only one label, preferably one that was not introduced by CIL.
* Scan a list of labels and return the data for the label that should be
* kept, and the remaining filtered list of labels *)
@@ -689,12 +735,16 @@ let labelsToKeep is_removable ll =
| true, ("", _) ->
(* keep this one only if we have no label so far *)
(ln, lab), false
- | true, _ -> sofar, false
+ | true, _ ->
+ sofar, false
| false, (_, lab') when is_removable lab' ->
(* this is an original label; prefer it to temporary or
* missing labels *)
(ln, lab), false
- | false, _ -> sofar, false
+ | false, (ln', _) when prefer ~new_label:ln ~old_label:ln' ->
+ (ln, lab), false
+ | false, _ ->
+ sofar, false
end
in
let newlabel', rest' = loop newlabel rest in
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index d1b82ba5bca85aca012627060eab778e5c30e68c..3377cdbb68d9e20a77b0aecff2ded641130ea2be 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -443,6 +443,16 @@ let append_loop_labels env =
Lenv.add_logic_label "LoopEntry" Logic_const.loop_entry_label
(Lenv.add_logic_label "LoopCurrent" Logic_const.loop_current_label env)
+let builtin_label = function
+ | "Init" -> Some Init
+ | "Pre" -> Some Pre
+ | "Old" -> Some Old
+ | "Post" -> Some Post
+ | "Here" -> Some Here
+ | "LoopCurrent" -> Some LoopCurrent
+ | "LoopEntry" -> Some LoopEntry
+ | _ -> None
+
let add_var var info env = Lenv.add_var var info env
let add_result env typ =
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index 8c07cf4093f40605fb125742d534d71591c80087..077a2556faf4addf7c12432356341e5152e06902 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -280,6 +280,10 @@ val append_pre_label: Lenv.t -> Lenv.t
*)
val append_init_label: Lenv.t -> Lenv.t
+(** returns the builtin label corresponding to the given name if it exists
+ @since Frama-C+dev
+*)
+val builtin_label: string -> logic_builtin_label option
(** adds a given variable in local environment. *)
val add_var: string -> logic_var -> Lenv.t -> Lenv.t
diff --git a/tests/syntax/clabels_builtin_labels.c b/tests/syntax/clabels_builtin_labels.c
new file mode 100644
index 0000000000000000000000000000000000000000..4295c77cec8efc7ebf28793330c35b2256e3172f
--- /dev/null
+++ b/tests/syntax/clabels_builtin_labels.c
@@ -0,0 +1,36 @@
+int x;
+
+void named(void){
+ x = 4;
+Init: Pre: Old: Post: Here: LoopCurrent: LoopEntry: A:;
+ x = 5;
+X: Y: ;
+ x = 6;
+Z: T: ;
+ x = 7;
+}
+
+void post_over_old_1(void){ Old: Post: ;}
+void post_over_old_2(void){ Post: Old: ;}
+
+void post_over_loop_1(void){ LoopEntry: Post: ;}
+void post_over_loop_2(void){ Post: LoopCurrent: ;}
+
+void post_over_other_1(void){ Here: Post: ;}
+void post_over_other_2(void){ Post: Pre: ;}
+void post_over_other_3(void){ Init: Post: Pre: ;}
+
+void old_over_loop_1(void){ LoopEntry: Old: ;}
+void old_over_loop_2(void){ Old: LoopCurrent: ;}
+
+void old_over_other_1(void){ Here: Old: ;}
+void old_over_other_2(void){ Old: Pre: ;}
+void old_over_other_3(void){ Init: Old: Pre: ;}
+
+void loop_over_other_1(void){ Here: LoopEntry: ;}
+void loop_over_other_2(void){ LoopCurrent: Pre: ;}
+void loop_over_other_3(void){ Init: LoopEntry: Pre: ;}
+
+void arbitray_other_1(void){ Here: Init: ;}
+void arbitray_other_2(void){ Init: Pre: ;}
+void arbitray_other_3(void){ Pre: Here: Init: ;}
diff --git a/tests/syntax/oracle/clabels_builtin_labels.res.oracle b/tests/syntax/oracle/clabels_builtin_labels.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..15a2a54f2b2111f5ac2c09b731d2ef1f7a872225
--- /dev/null
+++ b/tests/syntax/oracle/clabels_builtin_labels.res.oracle
@@ -0,0 +1,218 @@
+[kernel] Parsing clabels_builtin_labels.c (with preprocessing)
+[kernel] clabels_builtin_labels.c:5: Warning:
+ Init is a builtin ACSL label, this C label is hidden in annotations
+[kernel] clabels_builtin_labels.c:5: Warning:
+ Pre is a builtin ACSL label, this C label is hidden in annotations
+[kernel] clabels_builtin_labels.c:5: Warning:
+ Old is a builtin ACSL label, this C label is hidden in contracts
+[kernel] clabels_builtin_labels.c:5: Warning:
+ Post is a builtin ACSL label, this C label is hidden in contracts
+[kernel] clabels_builtin_labels.c:5: Warning:
+ Here is a builtin ACSL label, this C label is hidden in annotations
+[kernel] clabels_builtin_labels.c:5: Warning:
+ LoopCurrent is a builtin ACSL label, this C label is hidden in loop annotations
+[kernel] clabels_builtin_labels.c:5: Warning:
+ LoopEntry is a builtin ACSL label, this C label is hidden in loop annotations
+[kernel] clabels_builtin_labels.c:13: Warning:
+ Old is a builtin ACSL label, this C label is hidden in contracts
+[kernel] clabels_builtin_labels.c:13: Warning:
+ Post is a builtin ACSL label, this C label is hidden in contracts
+[kernel] clabels_builtin_labels.c:14: Warning:
+ Post is a builtin ACSL label, this C label is hidden in contracts
+[kernel] clabels_builtin_labels.c:14: Warning:
+ Old is a builtin ACSL label, this C label is hidden in contracts
+[kernel] clabels_builtin_labels.c:16: Warning:
+ LoopEntry is a builtin ACSL label, this C label is hidden in loop annotations
+[kernel] clabels_builtin_labels.c:16: Warning:
+ Post is a builtin ACSL label, this C label is hidden in contracts
+[kernel] clabels_builtin_labels.c:17: Warning:
+ Post is a builtin ACSL label, this C label is hidden in contracts
+[kernel] clabels_builtin_labels.c:17: Warning:
+ LoopCurrent is a builtin ACSL label, this C label is hidden in loop annotations
+[kernel] clabels_builtin_labels.c:19: Warning:
+ Here is a builtin ACSL label, this C label is hidden in annotations
+[kernel] clabels_builtin_labels.c:19: Warning:
+ Post is a builtin ACSL label, this C label is hidden in contracts
+[kernel] clabels_builtin_labels.c:20: Warning:
+ Post is a builtin ACSL label, this C label is hidden in contracts
+[kernel] clabels_builtin_labels.c:20: Warning:
+ Pre is a builtin ACSL label, this C label is hidden in annotations
+[kernel] clabels_builtin_labels.c:21: Warning:
+ Init is a builtin ACSL label, this C label is hidden in annotations
+[kernel] clabels_builtin_labels.c:21: Warning:
+ Post is a builtin ACSL label, this C label is hidden in contracts
+[kernel] clabels_builtin_labels.c:21: Warning:
+ Pre is a builtin ACSL label, this C label is hidden in annotations
+[kernel] clabels_builtin_labels.c:23: Warning:
+ LoopEntry is a builtin ACSL label, this C label is hidden in loop annotations
+[kernel] clabels_builtin_labels.c:23: Warning:
+ Old is a builtin ACSL label, this C label is hidden in contracts
+[kernel] clabels_builtin_labels.c:24: Warning:
+ Old is a builtin ACSL label, this C label is hidden in contracts
+[kernel] clabels_builtin_labels.c:24: Warning:
+ LoopCurrent is a builtin ACSL label, this C label is hidden in loop annotations
+[kernel] clabels_builtin_labels.c:26: Warning:
+ Here is a builtin ACSL label, this C label is hidden in annotations
+[kernel] clabels_builtin_labels.c:26: Warning:
+ Old is a builtin ACSL label, this C label is hidden in contracts
+[kernel] clabels_builtin_labels.c:27: Warning:
+ Old is a builtin ACSL label, this C label is hidden in contracts
+[kernel] clabels_builtin_labels.c:27: Warning:
+ Pre is a builtin ACSL label, this C label is hidden in annotations
+[kernel] clabels_builtin_labels.c:28: Warning:
+ Init is a builtin ACSL label, this C label is hidden in annotations
+[kernel] clabels_builtin_labels.c:28: Warning:
+ Old is a builtin ACSL label, this C label is hidden in contracts
+[kernel] clabels_builtin_labels.c:28: Warning:
+ Pre is a builtin ACSL label, this C label is hidden in annotations
+[kernel] clabels_builtin_labels.c:30: Warning:
+ Here is a builtin ACSL label, this C label is hidden in annotations
+[kernel] clabels_builtin_labels.c:30: Warning:
+ LoopEntry is a builtin ACSL label, this C label is hidden in loop annotations
+[kernel] clabels_builtin_labels.c:31: Warning:
+ LoopCurrent is a builtin ACSL label, this C label is hidden in loop annotations
+[kernel] clabels_builtin_labels.c:31: Warning:
+ Pre is a builtin ACSL label, this C label is hidden in annotations
+[kernel] clabels_builtin_labels.c:32: Warning:
+ Init is a builtin ACSL label, this C label is hidden in annotations
+[kernel] clabels_builtin_labels.c:32: Warning:
+ LoopEntry is a builtin ACSL label, this C label is hidden in loop annotations
+[kernel] clabels_builtin_labels.c:32: Warning:
+ Pre is a builtin ACSL label, this C label is hidden in annotations
+[kernel] clabels_builtin_labels.c:34: Warning:
+ Here is a builtin ACSL label, this C label is hidden in annotations
+[kernel] clabels_builtin_labels.c:34: Warning:
+ Init is a builtin ACSL label, this C label is hidden in annotations
+[kernel] clabels_builtin_labels.c:35: Warning:
+ Init is a builtin ACSL label, this C label is hidden in annotations
+[kernel] clabels_builtin_labels.c:35: Warning:
+ Pre is a builtin ACSL label, this C label is hidden in annotations
+[kernel] clabels_builtin_labels.c:36: Warning:
+ Pre is a builtin ACSL label, this C label is hidden in annotations
+[kernel] clabels_builtin_labels.c:36: Warning:
+ Here is a builtin ACSL label, this C label is hidden in annotations
+[kernel] clabels_builtin_labels.c:36: Warning:
+ Init is a builtin ACSL label, this C label is hidden in annotations
+/* Generated by Frama-C */
+int x;
+void named(void)
+{
+ x = 4;
+ A: ;
+ x = 5;
+ X: ;
+ x = 6;
+ Z: ;
+ x = 7;
+ return;
+}
+
+void post_over_old_1(void)
+{
+ Post: ;
+ return;
+}
+
+void post_over_old_2(void)
+{
+ Post: ;
+ return;
+}
+
+void post_over_loop_1(void)
+{
+ Post: ;
+ return;
+}
+
+void post_over_loop_2(void)
+{
+ Post: ;
+ return;
+}
+
+void post_over_other_1(void)
+{
+ Post: ;
+ return;
+}
+
+void post_over_other_2(void)
+{
+ Post: ;
+ return;
+}
+
+void post_over_other_3(void)
+{
+ Post: ;
+ return;
+}
+
+void old_over_loop_1(void)
+{
+ Old: ;
+ return;
+}
+
+void old_over_loop_2(void)
+{
+ Old: ;
+ return;
+}
+
+void old_over_other_1(void)
+{
+ Old: ;
+ return;
+}
+
+void old_over_other_2(void)
+{
+ Old: ;
+ return;
+}
+
+void old_over_other_3(void)
+{
+ Old: ;
+ return;
+}
+
+void loop_over_other_1(void)
+{
+ LoopEntry: ;
+ return;
+}
+
+void loop_over_other_2(void)
+{
+ LoopCurrent: ;
+ return;
+}
+
+void loop_over_other_3(void)
+{
+ LoopEntry: ;
+ return;
+}
+
+void arbitray_other_1(void)
+{
+ Here: ;
+ return;
+}
+
+void arbitray_other_2(void)
+{
+ Init: ;
+ return;
+}
+
+void arbitray_other_3(void)
+{
+ Pre: ;
+ return;
+}
+
+