[Ada] Postconditions in subprogram bodies

[Arnaud Charlet <charlet at adacore dot com>]

If a subprogram has postconditions, we generate a procedure to be invoked on
exit. that collects all postconditions specified for spec and body. If the
enclosing subprogram has no previous declarations, the generated procedure
must be attached to the enclosing body.

The following must compile quietly, and raise the proper exception at
execution:

gcc -c -gnata prepost.adb
---

procedure Prepost is
   procedure Post (X : Integer) is
      pragma Postcondition (X >= 0);
   begin
      null;
   end Post;
begin
  Post(-3);
end Prepost;

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

2010-01-25  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch6.adb (Process_PPCs): If a postcondition is present and the
	enclosing subprogram has no previous spec, attach postcondition
	procedure to the defining entity for the body.

Attachment: difs
Description: Text document