[Ada] Instances of Ada.Unchecked_Conversion as volatile functions

[Arnaud Charlet <charlet at adacore dot com>]

This patch implements the following rule from the SPARK RM:

   7.1.2 - (A protected function is also defined to be a volatile function,)
   as is an instance of Unchecked_Conversion where one or both of the actual
   Source and Target types are effectively volatile types.

-------------
--  Source --
-------------

--  gnat.adc

pragma SPARK_Mode (On);

--  volatile_uc.ads

with Ada.Unchecked_Conversion;

package Volatile_UC is
   type Rec is null record;
   type Vol_Rec_1 is null record with Volatile;
   type Vol_Rec_2 is null record with Volatile;

   function Rec_To_Vol is
     new Ada.Unchecked_Conversion (Rec, Vol_Rec_1);

   function Vol_To_Rec is
     new Ada.Unchecked_Conversion (Vol_Rec_1, Rec);

   function Vol_To_Vol is
     new Ada.Unchecked_Conversion (Vol_Rec_1, Vol_Rec_2);

   procedure Test_UC;
end Volatile_UC;

--  volatile_uc.adb

package body Volatile_UC is
   Rec_Obj   : Rec;
   Vol_Obj_1 : Vol_Rec_1;
   Vol_Obj_2 : Vol_Rec_2;

   procedure Test_UC is
      Obj_Ren   : Rec       renames Vol_To_Rec (Vol_Obj_1);
      Vol_Ren_1 : Vol_Rec_1 renames Rec_To_Vol (Rec_Obj);
      Vol_Ren_2 : Vol_Rec_2 renames Vol_To_Vol (Vol_Obj_1);
   begin null; end Test_UC;
end Volatile_UC;

-----------------
-- Compilation --
-----------------

$ gcc -c volatile_uc.adb

Tested on x86_64-pc-linux-gnu, committed on trunk

2015-10-23  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Analyze_Pragma): Pragma Volatile_Function should
	not apply to a function instantiation.
	* sem_util.adb (Has_Effectively_Volatile_Profile): New routine.
	(Is_Volatile_Function): An instance of Ada.Unchecked_Conversion
	is a volatile function when its profile contains an effectively
	volatile type.
	* sem_util.ads (Has_Effectively_Volatile_Profile): New routine.

Attachment: difs
Description: Text document