From c0a3ed4fac35bcc72ca3f2c0cd100aa6aab0e86d Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 3 Apr 2024 14:08:45 +0200
Subject: [PATCH] [typing] rename C labels when name clashes with a builtin
 ACSL label

---
 src/kernel_internals/typing/rmtmps.ml         | 16 ++++++++-
 .../oracle/clabels_builtin_labels.res.oracle  | 36 +++++++++----------
 2 files changed, 33 insertions(+), 19 deletions(-)

diff --git a/src/kernel_internals/typing/rmtmps.ml b/src/kernel_internals/typing/rmtmps.ml
index 58ea3289bda..960d954306a 100644
--- a/src/kernel_internals/typing/rmtmps.ml
+++ b/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 *)
diff --git a/tests/syntax/oracle/clabels_builtin_labels.res.oracle b/tests/syntax/oracle/clabels_builtin_labels.res.oracle
index 15a2a54f2b2..06e62cc85ea 100644
--- a/tests/syntax/oracle/clabels_builtin_labels.res.oracle
+++ b/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;
 }
 
-- 
GitLab