Merge pull request #253 from tjj2017/new_derived_type_checks

New derived type checks replaces PR #213

Author: chrisr-diffblue

gnat2goto/driver/tree_walk.adb

@@ -1487,9 +1487,11 @@ package body Tree_Walk is
       --  (via `Register_Type_Declaration') when its
       --  private or incomplete_type_declaration was processed.
       --  If it has no private declaration or the Incomplete_View is not
-      --  present then the full_type_declaration has to be registered
+      --  present or it is a derived_type_definition
+      --  then the full_type_declaration has to be registered
       if not (Has_Private_Declaration (E)
               or else Present (Incomplete_View (N)))
+        or else Nkind (Type_Definition (N)) = N_Derived_Type_Definition
       then
          Do_Type_Declaration (New_Type, E);
 

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()