[typing] rename C labels when name clashes with a builtin ACSL label

src/kernel_internals/typing/rmtmps.ml

@@ -720,6 +720,14 @@ let prefer ~new_label ~old_label =
       (* ok, now we give up: anything else is visible in code annotations *)
       | _ -> false
 
+(* 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 *)
@@ -730,7 +738,13 @@ 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 *)

tests/syntax/oracle/clabels_builtin_labels.res.oracle

@@ -109,109 +109,109 @@ void named(void)
 
 void post_over_old_1(void)
 {
-  Post: ;
+  __fc_user_label_Post: ;
   return;
 }
 
 void post_over_old_2(void)
 {
-  Post: ;
+  __fc_user_label_Post: ;
   return;
 }
 
 void post_over_loop_1(void)
 {
-  Post: ;
+  __fc_user_label_Post: ;
   return;
 }
 
 void post_over_loop_2(void)
 {
-  Post: ;
+  __fc_user_label_Post: ;
   return;
 }
 
 void post_over_other_1(void)
 {
-  Post: ;
+  __fc_user_label_Post: ;
   return;
 }
 
 void post_over_other_2(void)
 {
-  Post: ;
+  __fc_user_label_Post: ;
   return;
 }
 
 void post_over_other_3(void)
 {
-  Post: ;
+  __fc_user_label_Post: ;
   return;
 }
 
 void old_over_loop_1(void)
 {
-  Old: ;
+  __fc_user_label_Old: ;
   return;
 }
 
 void old_over_loop_2(void)
 {
-  Old: ;
+  __fc_user_label_Old: ;
   return;
 }
 
 void old_over_other_1(void)
 {
-  Old: ;
+  __fc_user_label_Old: ;
   return;
 }
 
 void old_over_other_2(void)
 {
-  Old: ;
+  __fc_user_label_Old: ;
   return;
 }
 
 void old_over_other_3(void)
 {
-  Old: ;
+  __fc_user_label_Old: ;
   return;
 }
 
 void loop_over_other_1(void)
 {
-  LoopEntry: ;
+  __fc_user_label_LoopEntry: ;
   return;
 }
 
 void loop_over_other_2(void)
 {
-  LoopCurrent: ;
+  __fc_user_label_LoopCurrent: ;
   return;
 }
 
 void loop_over_other_3(void)
 {
-  LoopEntry: ;
+  __fc_user_label_LoopEntry: ;
   return;
 }
 
 void arbitray_other_1(void)
 {
-  Here: ;
+  __fc_user_label_Here: ;
   return;
 }
 
 void arbitray_other_2(void)
 {
-  Init: ;
+  __fc_user_label_Init: ;
   return;
 }
 
 void arbitray_other_3(void)
 {
-  Pre: ;
+  __fc_user_label_Pre: ;
   return;
 }