Add support to access-to-object type

by simply creating a pointer-to type.

Note: this somehow was not triggered by our existing primitive-pointer
test (which had `int*`).

Author: petr-bauch

experiments/golden-results/StratoX-summary.txt

@@ -28,11 +28,6 @@ Calling function: Process_Pragma_Declaration
 Error message: Unknown pragma: volatile_full_access
 Nkind: N_Pragma
 --
-Occurs: 57 times
-Calling function: Do_Type_Definition
-Error message: Access type unsupported
-Nkind: N_Access_To_Object_Definition
---
 Occurs: 22 times
 Calling function: Do_Expression
 Error message: First of string unsupported
@@ -1755,7 +1750,7 @@ Error detected at REDACTED
 --
 Occurs: 3 times
 +===========================GNAT BUG DETECTED==============================+
-| GNU Ada (ada2goto) Assert_Failure tree_walk.adb:989                      |
+| GNU Ada (ada2goto) Assert_Failure tree_walk.adb:992                      |
 Error detected at REDACTED
 --
 Occurs: 2 times

experiments/golden-results/ksum-summary.txt

@@ -3,11 +3,6 @@ Calling function: Process_Pragma_Declaration
 Error message: Unsupported pragma: Suppress initialization
 Nkind: N_Pragma
 --
-Occurs: 1 times
-Calling function: Do_Type_Definition
-Error message: Access type unsupported
-Nkind: N_Access_To_Object_Definition
---
 Occurs: 41 times
 Redacted compiler error message:
 file "REDACTED" not found

experiments/golden-results/libkeccak-summary.txt

@@ -18,11 +18,6 @@ Calling function: Process_Declaration
 Error message: Use type clause declaration
 Nkind: N_Use_Type_Clause
 --
-Occurs: 19 times
-Calling function: Do_Type_Definition
-Error message: Access type unsupported
-Nkind: N_Access_To_Object_Definition
---
 Occurs: 18 times
 Calling function: Process_Pragma_Declaration
 Error message: Unsupported pragma: Suppress initialization

experiments/golden-results/libsparkcrypto-summary.txt

@@ -49,11 +49,6 @@ Error message: Non-literal bound unsupported
 Nkind: N_Defining_Identifier
 --
 Occurs: 24 times
-Calling function: Do_Type_Definition
-Error message: Access type unsupported
-Nkind: N_Access_To_Object_Definition
---
-Occurs: 24 times
 Calling function: Process_Declaration
 Error message: size clause not applied by the front-end
 Nkind: N_Attribute_Definition_Clause

experiments/golden-results/muen-summary.txt

@@ -3,11 +3,6 @@ Calling function: Process_Declaration
 Error message: Use type clause declaration
 Nkind: N_Use_Type_Clause
 --
-Occurs: 105 times
-Calling function: Do_Type_Definition
-Error message: Access type unsupported
-Nkind: N_Access_To_Object_Definition
---
 Occurs: 56 times
 Calling function: Process_Declaration
 Error message: size clause not applied by the front-end

gnat2goto/driver/tree_walk.adb

@@ -407,6 +407,9 @@ package body Tree_Walk is
      with Pre => Nkind (N) in N_Access_Function_Definition |
      N_Access_Procedure_Definition;
 
+   function Do_Access_To_Object_Definition (N : Node_Id) return Irep
+     with Pre => Nkind (N) = N_Access_To_Object_Definition;
+
    function Get_No_Return_Check return Irep;
 
    function Make_Malloc_Function_Call_Expr (Num_Elem : Irep;
@@ -5099,8 +5102,7 @@ package body Tree_Walk is
          when N_Access_Procedure_Definition =>
             return Do_Access_Function_Definition (N);
          when N_Access_To_Object_Definition =>
-            return Report_Unhandled_Node_Type (N, "Do_Type_Definition",
-                                               "Access type unsupported");
+            return Do_Access_To_Object_Definition (N);
          when others =>
             return Report_Unhandled_Node_Type (N, "Do_Type_Definition",
                                                "Unknown expression kind");
@@ -6281,6 +6283,17 @@ package body Tree_Walk is
                                                 Knr         => False));
    end Do_Access_Function_Definition;
 
+   function Do_Access_To_Object_Definition (N : Node_Id) return Irep
+   is
+      Sub_Indication : constant Node_Id := Subtype_Indication (N);
+      Under_Type : constant Node_Id := Etype
+        (if Nkind (Sub_Indication) = N_Subtype_Indication
+         then Subtype_Mark (Sub_Indication)
+         else Sub_Indication);
+   begin
+      return Make_Pointer_Type (Do_Type_Reference (Under_Type));
+   end Do_Access_To_Object_Definition;
+
    function Get_No_Return_Check return Irep is
       No_Return_Check_Symbol : constant Irep := Symbol_Expr
         (Get_Ada_Check_Symbol

testsuite/gnat2goto/tests/access-to-object/main.adb

@@ -0,0 +1,16 @@
+procedure Main is
+   type Day_Of_Month is range 1 .. 31;
+   type Day_Of_Month_Access is access all Day_Of_Month;
+
+   -- funny case where the subtype-indication has subtype-mark
+   type C_String_Ptr is access String (1 .. Positive'Last);
+
+   A : aliased Day_Of_Month;
+   Ptr1 : Day_Of_Month_Access := A'Access;
+   Ptr2 : Day_Of_Month_Access := A'Access;
+begin
+   Ptr1.all := 2;
+   pragma Assert (A=2); -- should succeed
+   Ptr2.all := 5;
+   pragma Assert (Ptr1.all=4); -- should fail
+end;

testsuite/gnat2goto/tests/access-to-object/test.out

@@ -0,0 +1,3 @@
+[main.assertion.1] line 13 assertion A=2: SUCCESS
+[main.assertion.2] line 15 assertion Ptr1.all=4: FAILURE
+VERIFICATION FAILED

testsuite/gnat2goto/tests/access-to-object/test.py

@@ -0,0 +1,3 @@
+from test_support import *
+
+prove()

testsuite/gnat2goto/tests/null_pointer/test.out

@@ -1,10 +1,2 @@
-Standard_Output from gnat2goto null_pointer:
-----------At: Do_Type_Definition----------
-----------Access type unsupported----------
-N_Access_To_Object_Definition (Node_Id=2262) (source)
-Parent = N_Full_Type_Declaration (Node_Id=2263)
-Sloc = 8232  null_pointer.adb:2:15
-Subtype_Indication = N_Identifier "integer" (Node_Id=2261)
-
 [null_pointer.assertion.1] line 5 assertion X = null: SUCCESS
 VERIFICATION SUCCESSFUL