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 <kirtc...@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.
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.
