[Ada] Preconditions and postconditions on subprogram bodies

[Ada] Preconditions and postconditions on subprogram bodies

[Arnaud Charlet]

[-- Attachment #1: Type: text/plain, Size: 970 bytes --]

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 #2: difs --]
[-- Type: text/plain, Size: 781 bytes --]

Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb	(revision 194777)
+++ sem_ch13.adb	(working copy)
@@ -1606,6 +1606,17 @@
 
                   if Nkind (Parent (N)) = N_Compilation_Unit then
                      Add_Global_Declaration (Aitem);
+
+                  --  If it is a subprogram body, add pragmas to list of
+                  --  declarations in body.
+
+                  elsif Nkind (N) = N_Subprogram_Body then
+                     if No (Declarations (N)) then
+                        Set_Declarations (N, New_List);
+                     end if;
+
+                     Append (Aitem, Declarations (N));
+
                   else
                      Insert_After (N, Aitem);
                   end if;