[kernel] simplify label name selection

- since we rename builtin labels, let us just try to find a label that does not need renaming

src/kernel_internals/typing/rmtmps.ml

@@ -674,51 +674,15 @@ 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 corresponds 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, select according to 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 original name did not correspond to a visible logic label,
-   and this is also the case for the selected one, or it was already masked
-   during the typing phase.
-*)
-
+(* 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 l_over ->
+  | Some _ ->
     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
+    | 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.

tests/syntax/oracle/clabels_builtin_labels.res.oracle

@@ -109,7 +109,7 @@ void named(void)
 
 void post_over_old_1(void)
 {
-  __fc_user_label_Post: ;
+  __fc_user_label_Old: ;
   return;
 }
 
@@ -121,7 +121,7 @@ void post_over_old_2(void)
 
 void post_over_loop_1(void)
 {
-  __fc_user_label_Post: ;
+  __fc_user_label_LoopEntry: ;
   return;
 }
 
@@ -133,7 +133,7 @@ void post_over_loop_2(void)
 
 void post_over_other_1(void)
 {
-  __fc_user_label_Post: ;
+  __fc_user_label_Here: ;
   return;
 }
 
@@ -145,13 +145,13 @@ void post_over_other_2(void)
 
 void post_over_other_3(void)
 {
-  __fc_user_label_Post: ;
+  __fc_user_label_Init: ;
   return;
 }
 
 void old_over_loop_1(void)
 {
-  __fc_user_label_Old: ;
+  __fc_user_label_LoopEntry: ;
   return;
 }
 
@@ -163,7 +163,7 @@ void old_over_loop_2(void)
 
 void old_over_other_1(void)
 {
-  __fc_user_label_Old: ;
+  __fc_user_label_Here: ;
   return;
 }
 
@@ -175,13 +175,13 @@ void old_over_other_2(void)
 
 void old_over_other_3(void)
 {
-  __fc_user_label_Old: ;
+  __fc_user_label_Init: ;
   return;
 }
 
 void loop_over_other_1(void)
 {
-  __fc_user_label_LoopEntry: ;
+  __fc_user_label_Here: ;
   return;
 }
 
@@ -193,7 +193,7 @@ void loop_over_other_2(void)
 
 void loop_over_other_3(void)
 {
-  __fc_user_label_LoopEntry: ;
+  __fc_user_label_Init: ;
   return;
 }