[Ada] Preconditions and Postconditions on generic subprograms.

[Arnaud Charlet <charlet at adacore dot com>]

This patch extends the use of pre- and postconditions to generic procedures
and functions. The checks are applied to every instance of the generic unit,
with the same visibility rules.

Executing:
   gnatmake -q -gnat05 genericppcm
   genericppcm

must yield:

   preconditionn violated in call
   postcondition violated in call
---
with genericppc;
with system.assertions; use system.assertions;
with text_io; use text_io;
procedure genericppcm is
   function g is new genericppc (integer);
   x : integer;
begin
   begin
      x := g (-1, -3);
      Put_Line (X'Img);
   exception
      when Assert_Failure =>
         Put_Line ("precondition violated in call");
   end;
   begin
      x := g (-1, -3);
      Put_Line (X'Img);
   exception
      when Assert_Failure =>
         Put_Line ("postcondition violated in call");
   end;
end;
---
generic
   type T_Item is private;
function genericppc (T : in t_Item; I : integer) return integer;
pragma Precondition (I > -2);
pragma Postcondition (genericppc'result > 0);
---
function genericppc (T : in t_Item; I : integer) return integer is
begin
   return -1;
end;

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


2008-07-31  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch6.adb (Analyze_Generic_Subprogram_Body): After analysis,
	transfer pre/postconditions from generic copy to original tree, so that
	they will appear in each instance.
	(Process_PPCs): Do not transform postconditions into a procedure in a
	generic context, to prevent double expansion of check pragmas.
	
	* sem_attr.adb: In an instance, the prefix of the 'result attribute
	can be the renaming of the
	current instance, so check validity of the name accordingly.

Attachment: difs
Description: Text document