[Ada] Rewrite check for SPARK RM 7.1.3(10)

[Pierre-Marie de Rodat <derodat at adacore dot com>]

The evolution of SPARK RM 7.1.3(10) rule was not followed by code that
implements it. The current wording is:

   "If a procedure has an in mode parameter of an effectively volatile type,
    then the Effective_Reads aspect of any corresponding actual parameter
    shall be False."

and the current code checks exactly that.

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

--  ineffective_actual.ads

with System;

package Ineffective_Actual
with
   SPARK_Mode
is
   type VT is 
      record
         Int : Integer;
      end record
   with Volatile;

   The_Volatile_Data : VT
   with
      Volatile,
      Async_Readers    => True,
      Async_Writers    => True,
      Effective_Reads  => False,
      Effective_Writes => False,
      Address => System'To_Address (16#1234_5678#);

   procedure Harmless_Reader (Data : in VT);

   procedure Do_Something;

end Ineffective_Actual;

--  ineffective_actual.adb

package body Ineffective_Actual
with
   SPARK_Mode
is
   procedure Harmless_Reader (Data : in VT)
   with
      SPARK_Mode => Off
   is
      I : Integer;
   begin
      I := Data.Int;
   end Harmless_Reader;

   procedure Do_Something
   is
   begin
      Harmless_Reader (The_Volatile_Data);
   end Do_Something;
end Ineffective_Actual;

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

& gcc -c ineffective_actual.adb
& gcc -c -gnatd.F ineffective_actual.adb

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

2017-10-09  Piotr Trojanek  <trojanek@adacore.com>

	* sem_res.adb (Property_Error): Remove.
	(Resolve_Actuals): check for SPARK RM 7.1.3(10) rewritten to match the
	current wording of the rule.

Attachment: difs
Description: Text document