Add tests for derived types

Author: tjj2017

testsuite/gnat2goto/tests/derived_private_type/derived_private_type.adb

@@ -0,0 +1,9 @@
+with Private_Type; use Private_Type;
+procedure Derived_Private_Type is
+   type Derived_Priv is new Priv;
+   V_Priv : Priv := Priv_Const;
+   V_D_Priv : Derived_Priv := Derived_Priv (Priv_Const);
+begin
+   pragma Assert (Derived_Priv (V_Priv) = V_D_Priv);
+   null;
+end Derived_Private_Type;

testsuite/gnat2goto/tests/derived_private_type/private_type.ads

@@ -0,0 +1,7 @@
+package Private_Type is
+   type Priv is private;
+   Priv_Const : constant Priv;
+private
+   type Priv is new Integer range 1 .. 23;
+   Priv_Const : constant Priv := 17;
+end Private_Type;

testsuite/gnat2goto/tests/derived_private_type/test.out

@@ -0,0 +1,2 @@
+[1] file derived_private_type.adb line 7 assertion: SUCCESS
+VERIFICATION SUCCESSFUL

testsuite/gnat2goto/tests/derived_private_type/test.py

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

testsuite/gnat2goto/tests/derived_types/derived_types.adb

@@ -0,0 +1,10 @@
+procedure Derived_Types is
+   type My_Int is range -23 .. 23;
+   type My_Real is new Float;
+   
+begin
+   pragma Assert (0 in My_Int);
+   pragma Assert (11.0 in My_Real);
+   pragma Assert (My_Int'Succ (22) = 23);
+   null;
+end Derived_Types;

testsuite/gnat2goto/tests/derived_types/test.out

@@ -0,0 +1,4 @@
+[1] file derived_types.adb line 6 assertion: SUCCESS
+[2] file derived_types.adb line 7 assertion: SUCCESS
+[3] file derived_types.adb line 8 assertion: SUCCESS
+VERIFICATION SUCCESSFUL

testsuite/gnat2goto/tests/derived_types/test.py

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