diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 4bd3d232a6e0eecef3971e71c3970df8eff36300..18bd9157b7d7915331c72ecfdbfce059d8b4501e 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
@@ -2777,7 +2777,7 @@ let makeGlobalVarinfo (isadef: bool) (vi: varinfo) : varinfo * bool =
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.*)
@@ -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..c07bfae94a550e5184603f83d025b164940c69f1 100644
--- a/src/kernel_internals/typing/rmtmps.ml
+++ b/src/kernel_internals/typing/rmtmps.ml
@@ -674,6 +674,24 @@ let markReferenced ast =
*
**********************************************************************)
+(* We prefer a label when it does not require renaming *)
+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 _ ->
+ match Logic_typing.builtin_label new_label with
+ | None -> true (* the old label is a builtin name, the new one is better *)
+ | Some _ -> false (* let us keep the old name *)
+
+(* if we're forced to keep a C label whose name match a builtin logic label,
+ we'll rename it to ensure no confusion can arise.
+ Since the original name is supposed to be unique in the function, and
+ users are not supposed to use symbols starting with an underscore, the chosen
+ name ought to be unique.
+*)
+let rename_c_label lab = "__fc_user_label_" ^ lab
+
(* 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 *)
@@ -684,17 +702,27 @@ let labelsToKeep is_removable ll =
let newlabel, keepl =
match l with
| Case _ | Default _ -> sofar, true
- | Label (ln, _, _) as lab -> begin
+ | Label (ln, loc, isuser) as lab ->
+ let lab =
+ match Logic_typing.builtin_label ln with
+ | None -> lab
+ | Some _ -> Label(rename_c_label ln, loc, isuser)
+ in
+ begin
match is_removable lab, sofar with
| 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..b7c98b2cbd0cf59dec64b00f2e235d637180ddb3
--- /dev/null
+++ b/tests/syntax/clabels_builtin_labels.c
@@ -0,0 +1,31 @@
+int x;
+
+void named_1(void){
+ x = 4;
+Init: Pre: Old: Post: Here: LoopCurrent: LoopEntry: A:;
+ x = 5;
+X: Y: ;
+ x = 6;
+Z: T: ;
+ x = 7;
+}
+
+void named_2(void){
+ x = 4;
+A: Init: Pre: Old: Post: Here: LoopCurrent: LoopEntry: ;
+ x = 5;
+X: Y: ;
+ x = 6;
+Z: T: ;
+ x = 7;
+}
+
+void named_3(void){
+ x = 4;
+Init: Pre: Old: Post: A: Here: LoopCurrent: LoopEntry: ;
+ x = 5;
+X: Y: ;
+ x = 6;
+Z: T: ;
+ x = 7;
+}
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..822f8f7853cb2a3dcc2fcac07e9d86b76864b5e6
--- /dev/null
+++ b/tests/syntax/oracle/clabels_builtin_labels.res.oracle
@@ -0,0 +1,82 @@
+[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:15: Warning:
+ Init is a builtin ACSL label, this C label is hidden in annotations
+[kernel] clabels_builtin_labels.c:15: Warning:
+ Pre is a builtin ACSL label, this C label is hidden in annotations
+[kernel] clabels_builtin_labels.c:15: Warning:
+ Old is a builtin ACSL label, this C label is hidden in contracts
+[kernel] clabels_builtin_labels.c:15: Warning:
+ Post is a builtin ACSL label, this C label is hidden in contracts
+[kernel] clabels_builtin_labels.c:15: Warning:
+ Here is a builtin ACSL label, this C label is hidden in annotations
+[kernel] clabels_builtin_labels.c:15: Warning:
+ LoopCurrent is a builtin ACSL label, this C label is hidden in loop annotations
+[kernel] clabels_builtin_labels.c:15: Warning:
+ LoopEntry is a builtin ACSL label, this C label is hidden in loop annotations
+[kernel] clabels_builtin_labels.c:25: Warning:
+ Init is a builtin ACSL label, this C label is hidden in annotations
+[kernel] clabels_builtin_labels.c:25: Warning:
+ Pre is a builtin ACSL label, this C label is hidden in annotations
+[kernel] clabels_builtin_labels.c:25: Warning:
+ Old is a builtin ACSL label, this C label is hidden in contracts
+[kernel] clabels_builtin_labels.c:25: Warning:
+ Post is a builtin ACSL label, this C label is hidden in contracts
+[kernel] clabels_builtin_labels.c:25: Warning:
+ Here is a builtin ACSL label, this C label is hidden in annotations
+[kernel] clabels_builtin_labels.c:25: Warning:
+ LoopCurrent is a builtin ACSL label, this C label is hidden in loop annotations
+[kernel] clabels_builtin_labels.c:25: Warning:
+ LoopEntry is a builtin ACSL label, this C label is hidden in loop annotations
+/* Generated by Frama-C */
+int x;
+void named_1(void)
+{
+ x = 4;
+ A: ;
+ x = 5;
+ X: ;
+ x = 6;
+ Z: ;
+ x = 7;
+ return;
+}
+
+void named_2(void)
+{
+ x = 4;
+ A: ;
+ x = 5;
+ X: ;
+ x = 6;
+ Z: ;
+ x = 7;
+ return;
+}
+
+void named_3(void)
+{
+ x = 4;
+ A: ;
+ x = 5;
+ X: ;
+ x = 6;
+ Z: ;
+ x = 7;
+ return;
+}
+
+
diff --git a/tools/lint/lint.ml b/tools/lint/lint.ml
index c0a576b75d00ab2ad223adea7e09a4286a989f79..cf0d18e5970e345f652c0aa4b13ec99c34e39f50 100644
--- a/tools/lint/lint.ml
+++ b/tools/lint/lint.ml
@@ -42,7 +42,7 @@ let external_formatters = [
available_cmd = "clang-format --version > /dev/null 2> /dev/null";
check_cmd = "clang-format --dry-run -Werror" ;
update_cmd = "clang-format -i" ;
- version_cmd = ""
+ version_cmd = "clang-format --version | grep -E '1[1-6]'"
}
;
{ kind = "Python";