[Ada] Changes to SPARK RM 7.1.3(11)

[Arnaud Charlet <charlet at adacore dot com>]

This patch implements a side effect of SPARK RM rule 7.1.3(11) which implies
that an effectively volatile formal parameter of mode out cannot be read.

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

--  async_writers_out.ads

package Async_Writers_Out with SPARK_Mode is
   type Volat_Array is array (1 .. 5) of Integer with Volatile;

   type Volat_Rec is record
      Id : Integer := 0;
   end record with Volatile;

   procedure Error_1 (Result : out Volat_Array);
   procedure Error_2 (Result : out Volat_Rec);
   procedure OK_1;
   procedure OK_2;
end Async_Writers_Out;

--  async_writers_out.adb

package body Async_Writers_Out with SPARK_Mode is
   Obj_1 : Volat_Array with Async_Readers, Async_Writers;
   Obj_2 : Volat_Rec   with Async_Readers, Async_Writers;

   procedure Reference_1 (Result : out Volat_Array);
   procedure Reference_2 (Result : out Volat_Rec);

   procedure Error_1 (Result : out Volat_Array) is
      Comp : constant Integer := Result (3);                         --  ERROR
   begin
      Result (1) := 1 + Result (5);                                  --  ERROR
   end Error_1;

   procedure Error_2 (Result : out Volat_Rec) is
      Comp : constant Integer := Result.Id;                          --  ERROR
   begin null; end Error_2;

   procedure OK_1 is
   begin
      Reference_1 (Obj_1);                                           --  OK
   end OK_1;

   procedure OK_2 is
   begin
      Reference_2 (Obj_2);                                           --  OK
   end OK_2;

   procedure Reference_1 (Result : out Volat_Array) is
   begin null; end Reference_1;

   procedure Reference_2 (Result : out Volat_Rec) is
   begin null; end Reference_2;
end Async_Writers_Out;

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

$ gcc -c async_writers_out.adb
async_writers_out.adb:9:34: illegal reading of volatile "out" parameter
async_writers_out.adb:11:25: volatile object cannot appear in this context
  (SPARK RM 7.1.3(13))
async_writers_out.adb:15:34: illegal reading of volatile "out" parameter

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

2015-01-06  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_res.adb (Is_Assignment_Or_Object_Expression): New routine.
	(Resolve_Actuals): An effectively volatile out
	parameter cannot act as an in or in out actual in a call.
	(Resolve_Entity_Name): An effectively volatile out parameter
	cannot be read.

Attachment: difs
Description: Text document