[Ada] Illegal use of SPARK volatile object not detected

[Arnaud Charlet <charlet at adacore dot com>]

This patch simplifies the entity resolution machinery which detects an illegaly
used SPARK volatile object with enabled external properties Async_Writers or
Effective_Reads. The mechanism no longer traverses the parent chain as this is
not needed.

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

--  volatile_use.ads

package Volatile_Use with SPARK_Mode => On is
   V1 : Integer
     with Volatile,
          Async_Writers => True;

   procedure Test_Eval_Order_OK (X : out Boolean)
     with Global => (Input => V1),
          Depends => (X => V1);

   procedure Test_Eval_Order_Bad1 (X : out Boolean)
     with Global => (Input => V1),
          Depends => (X => V1);

   procedure Test_Eval_Order_Bad2 (X : out Boolean)
     with Global => (Input => V1),
          Depends => (X => V1);
end Volatile_Use;

--  volatile_use.adb

package body Volatile_Use with SPARK_Mode => On is
   procedure Test_Eval_Order_OK (X : out Boolean) is
      T1 : Integer;
      T2 : Integer;
   begin
      T1 := V1;
      T2 := V1;
      X := (T1 <= T2);
   end Test_Eval_Order_OK;

   procedure Test_Eval_Order_Bad1 (X : out Boolean) is
      T1 : Integer;
   begin
      T1 := V1;
      X := (T1 <= V1);
   end Test_Eval_Order_Bad1;

   procedure Test_Eval_Order_Bad2 (X : out Boolean) is
   begin
      X := (V1 <= V1);
   end Test_Eval_Order_Bad2;
end Volatile_Use;

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

$ gcc -c volatile_use.adb
volatile_use.adb:15:19: volatile object cannot appear in this context (SPARK RM
  7.1.3(13))
volatile_use.adb:20:13: volatile object cannot appear in this context (SPARK RM
  7.1.3(13))
volatile_use.adb:20:19: volatile object cannot appear in this context (SPARK RM
  7.1.3(13))

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

2014-02-25  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_res.adb (Appears_In_Check): New routine.
	(Resolve_Entity_Name): Remove local variables Prev and
	Usage_OK. Par is now a constant. Remove the parent chain traversal
	as the placement of a volatile object with enabled property
	Async_Writers and/or Effective_Reads must appear immediately
	within a legal construct.

Attachment: difs
Description: Text document