[Ada] Discriminants and protected units

[Arnaud Charlet <charlet at adacore dot com>]

This patch implements the following SPARK RM rule:

   7.1.3(5) - An effectively volatile type other than a protected type shall
   not have a discriminated part.

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

--  discrims.ads

package Discrims with SPARK_Mode is
   type Vol_1 (Discr : Natural) is null record with Volatile;
   type Vol_2 (Discr : Natural) is null record;

   protected type Prot (Discr : Natural) is
      entry E;
   end Prot;
end Discrims;

--  discrims.adb

package body Discrims with SPARK_Mode is
   protected body Prot is
      entry E when True is begin null; end E;
   end Prot;

   Obj_1 : Vol_1 (1);
   Obj_2 : Vol_2 (2) with Volatile;
   Obj_3 : Prot  (3);
   Obj_4 : Prot  (4) with Volatile;
end Discrims;

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

$ gcc -c discrims.adb
discrims.adb:7:04: discriminated object "Obj_2" cannot be volatile
discrims.ads:2:09: discriminated type "Vol_1" cannot be volatile

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

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

	* sem_ch3.adb (Analyze_Object_Contract):
	A protected type or a protected object is allowed to have a
	discriminated part.

Attachment: difs
Description: Text document