Add new tests for implicit dereferencing.

Author: tjj2017

testsuite/gnat2goto/tests/pointer_to_array/pointer_to_array.adb

@@ -0,0 +1,78 @@
+procedure Pointer_To_Array is
+   type Count is range 0 .. 10;
+   subtype Index is Count range 1 .. Count'Last;
+
+   type Arr_T is array (Index) of Count;
+   type Arr_P is access all Arr_T;
+
+   type U_Arr_T is array (Integer range <>) of Integer;
+   type U_Arr_P is access all U_Arr_T;
+
+   Arr : aliased Arr_T;
+   Ptr : Arr_P;
+
+   U_Arr : aliased U_Arr_T := (1, 2, 3, 4);
+   U_Ptr : U_Arr_P;
+
+   C_dummy : Count;
+
+begin
+   for I in Index loop
+      Arr (I) := Index'Last - I + 1;
+   end loop;
+
+   for I in Index loop
+      pragma Assert (Arr (I) = Index'Last - I + 1);
+   end loop;
+
+   Ptr := Arr'Access;
+
+   for I in Index loop
+      pragma Assert (Ptr (I) = Index'Last - I + 1);
+   end loop;
+
+   for I in Index loop
+      Arr (I) := I;
+   end loop;
+
+   for I in Index loop
+      pragma Assert (Ptr (I) = I);
+   end loop;
+
+   for I in Index loop
+      pragma Assert (Arr (I) = I);
+   end loop;
+
+   pragma Assert (Arr (3) = 5);
+   pragma Assert (Ptr (5) = 3);
+   pragma Assert (Ptr.all (3) = 3);
+   pragma Assert (Ptr.all (3) = 5);
+
+  for I in Index loop
+      Ptr.all (I) := Index'Last - I + 1;
+   end loop;
+
+   for I in Index loop
+      pragma Assert (Ptr.all (I) = Index'Last - I + 1);
+   end loop;
+
+   for I in Index loop
+      pragma Assert (Arr (I) = Index'Last - I + 1);
+   end loop;
+
+   pragma Assert (Arr (1) = Index'Last);
+   pragma Assert (Ptr (Index'Last) = 1);
+   pragma Assert (Ptr.all (1) = Index'Last);
+   pragma Assert (Ptr.all (Index'Last) = 1);
+
+   pragma Assert (Ptr'Length = Index'Last);
+
+   U_Ptr := U_Arr'Access;
+   C_dummy := U_Ptr'Length;
+   C_dummy := Ptr'Length;
+
+   C_Dummy := Count (U_Ptr'First);
+   C_Dummy := Count (U_Ptr'Last);
+
+
+end Pointer_To_Array;

testsuite/gnat2goto/tests/pointer_to_array/test.py

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

testsuite/gnat2goto/tests/pointer_to_slice/pointer_to_slice.adb

@@ -0,0 +1,68 @@
+procedure Pointer_To_Slice is
+   type Count is range 0 .. 10;
+   subtype Index is Count range 1 .. Count'Last;
+
+   type Arr_T is array (Index) of Count;
+   type Arr_P is access all Arr_T;
+
+   Arr_1 : aliased Arr_T;
+   Arr_2 : aliased Arr_T := (others => 3);
+   Ptr_1 : Arr_P;
+   Ptr_2 : Arr_P;
+
+begin
+   for I in Index loop
+      Arr_1 (I) := I;
+   end loop;
+
+   for I in Index loop
+      pragma Assert (Arr_1 (I) = I);
+   end loop;
+
+   Arr_2 (1 .. 5) := Arr_1 (2 .. 6);
+
+   for I in Index range 1 .. 5 loop
+      pragma Assert (Arr_2 (I) = I + 1);
+   end loop;
+
+   for I in 6 .. Index'Last loop
+      pragma Assert (Arr_2 (I) = 3);
+   end loop;
+
+   Ptr_1 := Arr_1'Access;
+   Ptr_2 := Arr_2'Access;
+
+   for I in Index loop
+      pragma Assert (Ptr_1 (I) = I);
+   end loop;
+
+  for I in Index range 1 .. 5 loop
+      pragma Assert (Ptr_2 (I) = I + 1);
+   end loop;
+
+   for I in 6 .. Index'Last loop
+      pragma Assert (Ptr_2 (I) = 3);
+   end loop;
+
+   Ptr_1 (6 .. Index'Last) := Ptr_2 (6 .. Index'Last);
+
+   for I in Index range 1 .. 5 loop
+      pragma Assert (Arr_1 (I) = I);
+   end loop;
+
+   for I in 6 .. Index'Last loop
+      pragma Assert (Arr_1 (I) = 3);
+   end loop;
+
+   Ptr_2 (1 .. 5) := Ptr_1 (1 .. 5);
+
+   for I in Index range 1 .. 5 loop
+      pragma Assert (Arr_2 (I) = I);
+   end loop;
+
+   for I in 6 .. Index'Last loop
+      pragma Assert (Arr_2 (I) = 3);
+   end loop;
+
+
+end Pointer_To_Slice;

testsuite/gnat2goto/tests/pointer_to_slice/test.py

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

testsuite/gnat2goto/tests/record_access_type/pointer_to_slice.adb

@@ -0,0 +1,68 @@
+procedure Pointer_To_Slice is
+   type Count is range 0 .. 10;
+   subtype Index is Count range 1 .. Count'Last;
+
+   type Arr_T is array (Index) of Count;
+   type Arr_P is access all Arr_T;
+
+   Arr_1 : aliased Arr_T;
+   Arr_2 : aliased Arr_T := (others => 3);
+   Ptr_1 : Arr_P;
+   Ptr_2 : Arr_P;
+
+begin
+   for I in Index loop
+      Arr_1 (I) := I;
+   end loop;
+
+   for I in Index loop
+      pragma Assert (Arr_1 (I) = I);
+   end loop;
+
+   Arr_2 (1 .. 5) := Arr_1 (2 .. 6);
+
+   for I in Index range 1 .. 5 loop
+      pragma Assert (Arr_2 (I) = I + 1);
+   end loop;
+
+   for I in 6 .. Index'Last loop
+      pragma Assert (Arr_2 (I) = 3);
+   end loop;
+
+   Ptr_1 := Arr_1'Access;
+   Ptr_2 := Arr_2'Access;
+
+   for I in Index loop
+      pragma Assert (Ptr_1 (I) = I);
+   end loop;
+
+  for I in Index range 1 .. 5 loop
+      pragma Assert (Ptr_2 (I) = I + 1);
+   end loop;
+
+   for I in 6 .. Index'Last loop
+      pragma Assert (Ptr_2 (I) = 3);
+   end loop;
+
+   Ptr_1 (6 .. Index'Last) := Ptr_2 (6 .. Index'Last);
+
+   for I in Index range 1 .. 5 loop
+      pragma Assert (Arr_1 (I) = I);
+   end loop;
+
+   for I in 6 .. Index'Last loop
+      pragma Assert (Arr_1 (I) = 3);
+   end loop;
+
+   Ptr_2 (1 .. 5) := Ptr_1 (1 .. 5);
+
+   for I in Index range 1 .. 5 loop
+      pragma Assert (Arr_2 (I) = I);
+   end loop;
+
+   for I in 6 .. Index'Last loop
+      pragma Assert (Arr_2 (I) = 3);
+   end loop;
+
+
+end Pointer_To_Slice;

testsuite/gnat2goto/tests/record_access_type/test.py

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

testsuite/gnat2goto/tests/simple_access_Types/simple_access_types.adb

@@ -0,0 +1,15 @@
+procedure Simple_Access_Types is
+   type A_Int is access all Integer;
+
+   I : aliased Integer := 5;
+
+   Acc : A_Int;
+
+begin
+   pragma Assert (I = 5);
+   Acc := I'Access;
+   Acc.all := 3;
+  pragma Assert (I = 5);
+    pragma Assert (I = 3);
+
+end Simple_Access_Types;

testsuite/gnat2goto/tests/simple_access_Types/test.py

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