[Ada] Renamings of volatile objects

[Ada] Renamings of volatile objects

[Arnaud Charlet]

[-- Attachment #1: Type: text/plain, Size: 2476 bytes --]

This patch implements the following SPARK RM 7.1.3(12) rule:

   Contrary to the general SPARK 2014 rule that expression evaluation cannot
   have side effects, a read of an effectively volatile object with the
   properties Async_Writers or Effective_Reads set to True is considered to
   have an effect when read. To reconcile this discrepancy, a name denoting
   such an object shall only occur in a non-interfering context. A name occurs
   in a non-interfering context if it is:

      * the object_name of an object_renaming_declaration

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

--  volatile_renamings.ads

package Volatile_Renamings with SPARK_Mode is
   type Vol_Rec is record
      Comp : Integer;
   end record with Volatile;

   Vol_Obj_1 : Vol_Rec;
   Vol_Obj_2 : Integer with Volatile;

   Vol_Ren_1 : Vol_Rec renames Vol_Obj_1;
   Vol_Ren_2 : Integer renames Vol_Obj_2;

   function Rec_Func return Vol_Rec with Volatile_Function;
   function Int_Func return Integer with Volatile_Function;

   function Error_Rec_Func return Vol_Rec;
   function Error_Int_Func return Integer;
end Volatile_Renamings;

--  volatile_renamings.adb

package body Volatile_Renamings with SPARK_Mode is
   function Rec_Func return Vol_Rec is
   begin
      return Vol_Ren_1;                                              --  OK
   end Rec_Func;

   function Int_Func return Integer is
   begin
      return Vol_Ren_2;                                              --  OK
   end Int_Func;

   function Error_Rec_Func return Vol_Rec is
   begin
      return Vol_Ren_1;                                              --  Error
   end Error_Rec_Func;

   function Error_Int_Func return Integer is
   begin
      return Vol_Ren_2;                                              --  Error
   end Error_Int_Func;
end Volatile_Renamings;

----------------------------
-- Compilation and output --
----------------------------

$ gcc -c volatile_renamings.adb
volatile_renamings.adb:14:14: volatile object cannot appear in this context
  (SPARK RM 7.1.3(12))
volatile_renamings.adb:19:14: volatile object cannot appear in this context
  (SPARK RM 7.1.3(12))
volatile_renamings.ads:15:13: nonvolatile function "Error_Rec_Func" cannot have
  a volatile return type

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

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

	* sem_res.adb (Is_OK_Volatile_Context): A volatile object may appear
	in an object declaration as long as it denotes the name.


[-- Attachment #2: difs --]
[-- Type: text/plain, Size: 614 bytes --]

Index: sem_res.adb
===================================================================
--- sem_res.adb	(revision 229362)
+++ sem_res.adb	(working copy)
@@ -6993,6 +6993,13 @@
                return True;
             end if;
 
+         --  The volatile object acts as the name of a renaming declaration
+
+         elsif Nkind (Context) = N_Object_Renaming_Declaration
+           and then Name (Context) = Obj_Ref
+         then
+            return True;
+
          --  The volatile object appears as an actual parameter in a call to an
          --  instance of Unchecked_Conversion whose result is renamed.