[Ada] Preconditions and postconditions on subprogram bodies

[Arnaud Charlet <charlet at adacore dot com>]

This patch implements properly pre- and postconditions that are given in
subprogram bodies that have no previous specification.

Executing:

   gnatmake -q -gnat12a pre_on_baas
   pre_on_baas

must yield:

before
P called
after

--
pragma Ada_2012;
pragma Check_Policy (Precondition, Check);
with Ada.Text_IO; use Ada.Text_IO;

procedure Pre_On_BaaS is

   function F (S : String)  return Boolean is
   begin
      Put_Line (S);
      return True;
   end F;

   procedure P with
      Pre => F ("before"),
      Post => F ("after")
   is
   begin
      Put_Line ("P called");
   end P;

begin
   P;
end Pre_On_BaaS;

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

2013-01-02  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch13.adb (Analyze_Aspect_Specifications): If the aspect
	appears on a subprogram body that acts as a spec, place the
	corresponding pragma in the declarations of the body, so that
	e.g. pre/postcondition checks can be generated appropriately.

Attachment: difs
Description: Text document