Tests for 'use type' & 'use all type' clause

NB our package implementation does not support function calls atm, so 
although 'use type' can work fully if only built-in operators are used, 
any use of functions or overloaded operators or new 'basic operations' 
for a custom type will fail.

Author: Sonny Martin

testsuite/gnat2goto/tests/package_use_type_N_Use_Type_Clause/Use_Type_Clause.adb

@@ -0,0 +1,19 @@
+package body Count_Types is
+   ------------------------------------------------------------
+   function "=" (X : Counter; Y: Integer) return Boolean is
+   begin
+      if X.Value = Y then
+         return True;
+      else
+         return False;
+      end if;
+   end "=";
+   ------------------------------------------------------------
+   function Double (X : in out Counter) return Counter is
+   begin
+      X.Value := X.Value + X.Value;
+      --  return X.Value + X.Value;
+      return X;
+   end Double;
+   ------------------------------------------------------------
+end Count_Types;

testsuite/gnat2goto/tests/package_use_type_N_Use_Type_Clause/count_types.adb

@@ -0,0 +1,13 @@
+package Count_Types is
+   type Count is new Integer;
+   ------------------------------------------------------------
+   type Counter is
+      record
+         Value : Integer := 1;
+      end record;
+
+   function "=" (X : Counter; Y : Integer) return Boolean;
+
+   function Double (X : in out Counter) return Counter;
+   ------------------------------------------------------------
+end Count_Types;

testsuite/gnat2goto/tests/package_use_type_N_Use_Type_Clause/count_types.ads

@@ -0,0 +1,3 @@
+**** WARNING: no body for function count_types__double
+[1] file use_type_clause.adb line 16 assertion: SUCCESS
+VERIFICATION SUCCESSFUL

testsuite/gnat2goto/tests/package_use_type_N_Use_Type_Clause/external_types.ads

@@ -0,0 +1,21 @@
+--  'use type' clause makes visible only the operators associated with a type
+--  (NB but not the type itself, this must still be fully qualified
+with Count_Types; use type Count_Types.Count;
+
+--  'use all type' clause makes visible both the operators and primitive
+--  operations associated with a type (NB but not the type itself, this must
+--  still be fully qualified)
+with Count_Types; use all type Count_Types.Counter;
+
+procedure Use_Type_Clause is
+   A : Count_Types.Count := 1;
+
+   B : Count_Types.Counter;
+   C : Count_Types.Counter;
+begin
+   pragma Assert (A=1);
+
+   C := Double(B);  --  Double is accessible due to 'use all type' clause
+   --  next statement would fail as packages do not support function calls atm
+   --  pragma Assert (C=2);
+end Use_Type_Clause;