[Ada] Implementation of Ada2012 rules on preconditions for null procedures

[Ada] Implementation of Ada2012 rules on preconditions for null procedures

[Arnaud Charlet]

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

Ada Issue AI05-0230 specifies that null procedures can only have inheritable
'Class preconditions. For compatibility with the earlier GNAT pragmas for
preconditions, this rule only applies to Ada2012 aspect specifications.

Compilation of p.ads must yield:

    p.ads:5:06: aspect "Pre" requires 'Class for null procedure
    p.ads:17:05: aspect "Pre" requires 'Class for abstract subprogram

---
package P is
   type I is interface;
   procedure Proc (Obj : I) is null
   with
     Pre => False;         --  ERROR

  procedure Proc2 (Obj : in out I) is null
  with
    Pre'Class => False;    --  OK

  procedure Proc3 (Obj : in out I) is abstract
  with
    Pre'Class => False;    --  OK

  procedure Proc4 (Obj : in out I) is abstract
  with
    Pre => False;    --  ERROR

 procedure Proc5 (Obj : out I) is null;
 pragma Precondition (False);    --  OK. GNAT pragma
end P;

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

2011-08-02  Ed Schonberg  <schonberg@adacore.com>

	* sem_prag.adb (Chain_PPC): Implement AI04-0230: null procedures can
	only have inheritable classwide pre/postconditions.


[-- Attachment #2: difs --]
[-- Type: text/plain, Size: 1099 bytes --]

Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 177157)
+++ sem_prag.adb	(working copy)
@@ -1595,6 +1595,19 @@
                     ("aspect % requires ''Class for abstract subprogram");
                end if;
 
+            --  AI05-0230:  the same restriction applies to null procedures.
+            --  For compatibility with earlier uses of the Ada pragma, apply
+            --  this rule only to aspect specifications.
+
+            elsif Nkind (PO) = N_Subprogram_Declaration
+              and then Nkind (Specification (PO)) = N_Procedure_Specification
+              and then Null_Present (Specification (PO))
+              and then From_Aspect_Specification (N)
+              and then not Class_Present (N)
+            then
+               Error_Pragma
+                 ("aspect % requires ''Class for null procedure");
+
             elsif not Nkind_In (PO, N_Subprogram_Declaration,
                                     N_Generic_Subprogram_Declaration,
                                     N_Entry_Declaration)