[Ada] Aspect/pragma Extensions_Visible

[Arnaud Charlet <charlet at adacore dot com>]

This patch implements aspect/pragma Extensions_Visible. This construct has the
following rules:

Extensions_Visible is a Boolean-valued aspect which may be specified for a
subprogram. If directly specified, the aspect_definition shall be a static
[Boolean] expression. The aspect is inherited by an inherited primitive
subprogram. If the aspect is neither inherited nor directly specified for a
subprogram, then the aspect is False.

If the Extensions_Visible aspect is False for a subprogram, then certain
restrictions are imposed on the use of any parameter of the subprogram which is
of a specific tagged type (or of a private type whose full view is a specific
tagged type). Such a parameter shall not be converted implicitly or explicitly
to a class-wide type. Such a parameter shall not be passed as an actual
parameter in a call to a subprogram whose Extensions_Visible aspect is True.
These restrictions also apply to any parenthesized expression, qualified
expression, or type conversion whose operand is subject to these restrictions,
and to any conditional expression having at least one dependent_expression
which is subject to these restrictions.

A subprogram whose Extensions_Visible aspect is True shall not override an
inherited primitive operation of a tagged type whose Extensions_Visible aspect
is False.

If a nonnull type extension inherits a procedure having both a False
Extensions_Visible aspect and one or more controlling out-mode parameters, then
the inherited procedure requires overriding.

The Extensions_Visible aspect shall not be specified for a subprogram which has
no parameters of either a specific tagged type or a private type unless the
subprogram is declared in an instance of a generic unit and the corresponding
subprogram in the generic unit satisfies this rule.

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

--  extensions_visible_illegal_2.ads

package Extensions_Visible_Illegal_2 with SPARK_Mode is
   type T is tagged record
      X : Integer;
   end record;

   procedure Proc   (Param : in T);
   procedure Proc_2 (Param : out T) with Extensions_Visible => False;

   type Extension is new T with record
      Y : Integer;
   end record;

   overriding procedure Proc (Param : in Extension) with Extensions_Visible;

   type Null_Extension is new T with null record;

   overriding procedure Proc (Param : in Null_Extension)
     with Extensions_Visible;
end Extensions_Visible_Illegal_2;

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

$ gcc -c extensions_visible_illegal_2.ads
extensions_visible_illegal_2.ads:9:09: type must be declared abstract or
  "Proc_2" overridden
extensions_visible_illegal_2.ads:9:09: "Proc_2" at line 7 is subject to
  Extensions_Visible False
extensions_visible_illegal_2.ads:13:25: subprogram "Proc" with
  Extensions_Visible True cannot override subprogram at line 6 with
  Extensions_Visible False
extensions_visible_illegal_2.ads:17:25: subprogram "Proc" with
  Extensions_Visible True cannot override subprogram at line 6 with
  Extensions_Visible False

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

2014-10-30  Hristian Kirtchev  <kirtchev@adacore.com>

	* aspects.adb: Add an entry for aspect Extensions_Visible in
	table Canonical_Aspect.
	* aspects.ads: Add entry for aspect Extensions_Visible in
	tables Aspect_Argument, Aspect_Delay, Aspect_Id, Aspect_Names,
	Implementation_Defined_Aspect.
	* einfo.adb (Get_Pragma): Include pragma Extensions_Visible in
	the list of contract pragmas.
	* par-prag.adb Pragma Extensions_Visible does not require special
	processing from the parser.
	* sem_ch3.adb (Analyze_Object_Declaration): Prevent an
	implicit class-wide conversion of a formal parameter
	of a specific tagged type whose related subprogram is
	subject to pragma Extensions_Visible with value "False".
	(Check_Abstract_Overriding): Add various overriding checks
	related to pragma Extensions_Visible.
	(Derive_Subprogram):
	A subprogram subject to pragma Extensions_Visible with value
	False requires overriding if the subprogram has at least one
	controlling OUT parameter.
	(Is_EVF_Procedure): New routine.
	* sem_ch4.adb (Analyze_Type_Conversion): A formal parameter of
	a specific tagged type whose related subprogram is subject to
	pragma Extensions_Visible with value "False" cannot appear in
	a class-wide conversion.
	* sem_ch6.adb (Analyze_Subprogram_Contract): Remove
	the assertion to account for pragma Extensions_Visible.
	(Check_Overriding_Indicator): An overriding subprogram
	inherits the contact of the overridden subprogram.
	(New_Overloaded_Entity): An overriding subprogram inherits the
	contact of the overridden subprogram.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Add processing
	for aspect Extensions_Visible.
	(Check_Aspect_At_Freeze_Point): Aspect Extensions_Visible does not
	require special processing at the freeze point.
	* sem_prag.adb Add an entry for pragma Extensions_Visible in
	table Sig_Flags.
	(Analyze_Pragma): Ensure that various SPARK
	pragmas lack identifiers in their arguments. Add processing for
	pragma Extensions_Visible.
	(Chain_CTC): Code reformatting.
	* sem_res.adb (Resolve_Actuals): A formal parameter of a
	specific tagged type whose related subprogram is subject to
	pragma Extensions_Visible with value "False" cannot act as an
	actual in a subprogram with value "True".
	* sem_util.adb (Add_Classification): New routine.
	(Add_Contract_Item): Account for pragma Extensions_Visible. Code
	reformatting.
	(Add_Contract_Test_Case): New routine.
	(Add_Pre_Post_Condition): New routine.
	(Extensions_Visible_Status): New routine.
	(Inherit_Subprogram_Contract): New routine.
	(Is_EVF_Expression): New routine.
	(Is_Specific_Tagged_Type): New routine.
	* sem_util.ads Add type Extensions_Visible_Mode and document all values.
	(Add_Contract_Item): Add pragma Extensions_Visible to the
	comment on usage.
	(Inherit_Subprogram_Contract): New routine.
	(Is_EVF_Expression): New routine.
	(Is_Specific_Tagged_Type): New routine.
	* sinfo.adb (Is_Inherited): New routine.
	(Set_Is_Inherited): New routine.
	* sinfo.ads Add flag Is_Inherited along with its usage in
	nodes.
	(Is_Inherited): New routine along with pragma Inline.
	(Set_Is_Inherited): New routine along with pragma Inline.
	* snames.ads-tmpl: Add predefined name "Extensions_Visible"
	and a new Pragma_Id for the pragma.

Attachment: difs
Description: Text document