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 <schonb...@adacore.com>
* sem_prag.adb (Chain_PPC): Implement AI04-0230: null procedures can
only have inheritable classwide pre/postconditions.
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)
