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 <kirtc...@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.
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 229231)
+++ sem_prag.adb (working copy)
@@ -21543,14 +21543,9 @@
Subp_Decl :=
Find_Related_Subprogram_Or_Body (N, Do_Checks => True);
- -- Function instantiation
-
- if Nkind (Subp_Decl) = N_Function_Instantiation then
- null;
-
-- Generic subprogram
- elsif Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then
+ if Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then
null;
-- Body acts as spec
@@ -21578,7 +21573,6 @@
end if;
Spec_Id := Corresponding_Spec_Of (Subp_Decl);
- Over_Id := Overridden_Operation (Spec_Id);
if not Ekind_In (Spec_Id, E_Function, E_Generic_Function) then
Pragma_Misplaced;
@@ -21595,6 +21589,8 @@
-- in New_Overloaded_Entity, however at that point the pragma has
-- not been processed yet.
+ Over_Id := Overridden_Operation (Spec_Id);
+
if Present (Over_Id)
and then not Is_Volatile_Function (Over_Id)
then
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 229234)
+++ sem_util.adb (working copy)
@@ -2108,9 +2108,7 @@
T := Full_View (T);
end if;
- if Is_Descendent_Of_Address (T)
- or else Is_Limited_Type (T)
- then
+ if Is_Descendent_Of_Address (T) or else Is_Limited_Type (T) then
Set_Is_Pure (Subp_Id, False);
exit;
end if;
@@ -8552,6 +8550,39 @@
return False;
end Has_Discriminant_Dependent_Constraint;
+ --------------------------------------
+ -- Has_Effectively_Volatile_Profile --
+ --------------------------------------
+
+ function Has_Effectively_Volatile_Profile
+ (Subp_Id : Entity_Id) return Boolean
+ is
+ Formal : Entity_Id;
+
+ begin
+ -- Inspect the formal parameters looking for an effectively volatile
+ -- type.
+
+ Formal := First_Formal (Subp_Id);
+ while Present (Formal) loop
+ if Is_Effectively_Volatile (Etype (Formal)) then
+ return True;
+ end if;
+
+ Next_Formal (Formal);
+ end loop;
+
+ -- Inspect the return type of functions
+
+ if Ekind_In (Subp_Id, E_Function, E_Generic_Function)
+ and then Is_Effectively_Volatile (Etype (Subp_Id))
+ then
+ return True;
+ end if;
+
+ return False;
+ end Has_Effectively_Volatile_Profile;
+
--------------------------
-- Has_Enabled_Property --
--------------------------
@@ -13721,6 +13752,14 @@
then
return True;
+ -- An instance of Ada.Unchecked_Conversion is a volatile function if
+ -- either the source or the target are effectively volatile.
+
+ elsif Is_Unchecked_Conversion_Instance (Func_Id)
+ and then Has_Effectively_Volatile_Profile (Func_Id)
+ then
+ return True;
+
-- Otherwise the function is treated as volatile if it is subject to
-- enabled pragma Volatile_Function.
Index: sem_util.ads
===================================================================
--- sem_util.ads (revision 229234)
+++ sem_util.ads (working copy)
@@ -1006,6 +1006,11 @@
-- Returns True if and only if Comp has a constrained subtype that depends
-- on a discriminant.
+ function Has_Effectively_Volatile_Profile
+ (Subp_Id : Entity_Id) return Boolean;
+ -- Determine whether subprogram Subp_Id has an effectively volatile formal
+ -- parameter or returns an effectively volatile value.
+
function Has_Infinities (E : Entity_Id) return Boolean;
-- Determines if the range of the floating-point type E includes
-- infinities. Returns False if E is not a floating-point type.
