Decorate addressed variables

with dollar sign and via a helper function.

Author: petr-bauch

gnat2goto/driver/tree_walk.adb

@@ -4712,20 +4712,20 @@ package body Tree_Walk is
                Address_Expr : constant Irep := Get_Address_Expr;
                Address_Type : constant Irep :=
                  Make_Pointer_Type (Target_Type_Irep);
+               Decorated_Name : constant String :=
+                 Decorate_Addressed_Variables (Get_Identifier (Target_Name));
                Lhs_Expr : constant Irep :=
                  Make_Symbol_Expr (Source_Location => Source_Loc,
                                    I_Type          => Address_Type,
                                    Range_Check     => False,
-                                   Identifier      =>
-                                     "Ptr_" & Get_Identifier (Target_Name));
+                                   Identifier      => Decorated_Name);
                Rhs_Expr : constant Irep :=
                  Typecast_If_Necessary (Expr     => Address_Expr,
                                         New_Type => Address_Type,
                                         A_Symbol_Table => Global_Symbol_Table);
             begin
                New_Object_Symbol_Entry
-                 (Object_Name       =>
-                    Intern ("Ptr_" & Get_Identifier (Target_Name)),
+                 (Object_Name       => Intern (Decorated_Name),
                   Object_Type       => Address_Type,
                   Object_Init_Value => Rhs_Expr,
                   A_Symbol_Table    => Global_Symbol_Table);

gnat2goto/ireps/ireps_generator.py

@@ -1878,6 +1878,10 @@ def generate_code(self, optimize, schema_file_names):
         write(s, "--  Increase Pointer Depth")
         write(s, "")
 
+        write(s, "function Decorate_Addressed_Variables (Name : String) return String;")
+        write(s, "--  Create Decorated Name")
+        write(s, "")
+
         write(s, "function Remove_Extra_Type_Information (I : Irep) return Irep;")
         write(s, "--  Remove Type Bounds")
         write(s, "")
@@ -2130,7 +2134,8 @@ def generate_code(self, optimize, schema_file_names):
         with indent(b):
             write(b, "return Make_Dereference_Expr (Make_Symbol_Expr (Get_Source_Location (I),")
             with indent(b):
-                write(b, "Make_Pointer_Type (Get_Type (I), 64), False, \"Ptr_\" & Name),")
+                write(b, "Make_Pointer_Type (Get_Type (I), 64), False,")
+                write(b, "Decorate_Addressed_Variables (Name)),")
                 write(b, "Get_Source_Location (I), Get_Type (I));")
         write(b, "end if;")
         write(b, "")
@@ -2151,6 +2156,15 @@ def generate_code(self, optimize, schema_file_names):
         write(b, "end Wrap_Pointer;")
         write(b, "")
 
+        write_comment_block(b, "Decorate_Addressed_Variables")
+        write(b, "function Decorate_Addressed_Variables (Name : String) return String")
+        write(b, "is")
+        write(b, "begin")
+        with indent(b):
+            write(b, "return Name & \"$Ptr\";")
+        write(b, "end Decorate_Addressed_Variables;")
+        write(b, "")
+
         write_comment_block(b, "Remove_Extra_Type_Information")
         write(b, "function Remove_Extra_Type_Information (I : Irep) return Irep")
         write(b, "is")