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

testsuite/gnat2goto/tests/package_use_type_N_Use_Type_Clause/count_types.adb

@@ -0,0 +1,8 @@
+package body Count_Types is
+
+   function Double (X : in out Counter) return Counter is
+   begin
+      return X*2;
+   end Double;
+
+end Count_Types;

testsuite/gnat2goto/tests/package_use_type_N_Use_Type_Clause/count_types.ads

@@ -0,0 +1,8 @@
+package Count_Types is
+
+   type Count is new Integer;
+
+   type Counter is new Integer;
+   function Double (X : in out Counter) return Counter;
+
+end Count_Types;

testsuite/gnat2goto/tests/package_use_type_N_Use_Type_Clause/test.out

@@ -0,0 +1,7 @@
+VERIFICATION SUCCESSFUL
+Error from cbmc use_type_clause:
+**** WARNING: no body for function count_types__double
+
+[1] file use_type_clause.adb line 21 assertion: SUCCESS
+[2] file use_type_clause.adb line 24 assertion: FAILURE
+VERIFICATION FAILED

testsuite/gnat2goto/tests/package_use_type_N_Use_Type_Clause/use_type_clause.adb

@@ -0,0 +1,25 @@
+--  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.
+----------------------------------------------------------------------
+
+--  '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 :=1;
+begin
+   pragma Assert (A=1);
+
+   B := Double(B);  --  Double is visible due to the 'use all type' clause
+   pragma Assert(B=2);
+end Use_Type_Clause;