[Ada] Implement new pragmas Pre[_Class] and Post[_Class]

This implements four new pragmas, Pre, Pre_Class, Post, Post_Class
that are intended to closely mirrir the four corresponding aspects
Pre, Pre'Class, Post, and Post'Class. They inherit the same set of
restrictions as these aspects. In particular, a given aspect can be
specified only once for a given entity (using either an aspect or
a pragma, but not both), and they can be given for a body only if
there is no separate specification. Unlike pragmas Precondition
and Postcondition, they take only one parameter (the expression)
and it must appear without an identifier.

The following example shows Pre and Post in action (and also shows
that they are controlled by assertion identifiers of the same name
(Pre_Class and Post_Class are controlled by Pre'Class/Post'Class).

      1. with Ada.Exceptions; use Ada.Exceptions;
      2. with Text_IO; use Text_IO;
      3. procedure PostPrePrag is
      4. begin
      5.    declare
      6.       pragma Assertion_Policy (Pre => Check, Post => Check);
      7.       function F (A : Integer) return Integer;
      8.       pragma Pre (A in 1 .. 10);
      9.       pragma Post (F'Result < 10);
     10.
     11.       function F (A : Integer) return Integer is
     12.       begin
     13.          return 2 * A;
     14.       end;
     15.
     16.       F1, F2, F3 : Integer;
     17.    begin
     18.       F1 := F (2);
     19.       Put_Line ("OK1");
     20.
     21.       begin
     22.          F2 := F (9);
     23.          Put_Line ("ERROR1");
     24.       exception
     25.          when M : others =>
     26.             Put_Line ("OK2 " & Exception_Message (M));
     27.       end;
     28.
     29.       begin
     30.          F3 := F (12);
     31.          Put_Line ("ERROR2");
     32.       exception
     33.          when M : others =>
     34.             Put_Line ("OK3 " & Exception_Message (M));
     35.       end;
     36.    end;
     37.
     38.    declare
     39.       pragma Assertion_Policy (Pre => Ignore, Post => Ignore);
     40.       function F (A : Integer) return Integer;
     41.       pragma Pre (A in 1 .. 10);
     42.       pragma Post (F'Result < 10);
     43.
     44.       function F (A : Integer) return Integer is
     45.       begin
     46.          return 2 * A;
     47.       end;
     48.
     49.       F1, F2, F3 : Integer;
     50.    begin
     51.       F1 := F (2);
     52.       Put_Line ("OK4");
     53.
     54.       begin
     55.          F2 := F (9);
     56.          Put_line ("OK5");
     57.       exception
     58.          when M : others =>
     59.             Put_Line ("ERROR3 " & Exception_Message (M));
     60.       end;
     61.
     62.       begin
     63.          F3 := F (12);
     64.          Put_Line ("OK6");
     65.       exception
     66.          when M : others =>
     67.             Put_Line ("ERROR4 " & Exception_Message (M));
     68.       end;
     69.    end;
     70.
     71. end PostPrePrag;

The output of the above example is:

OK1
OK2 failed postcondition from postpreprag.adb:9
OK3 failed precondition from postpreprag.adb:8
OK4
OK5
OK6

The following example shows additional error checking that
applies to these pragmas (if Precondition and Postcondition
were used in place of Pre and Post, these errors would not
be flagged):

      1. procedure PostPrePragE is
      2.    pragma Assertion_Policy (Pre => Check, Post => Check);
      3.    function F (A : Integer) return Integer
      4.      with Pre => A = 10;
      5.    pragma Pre (A in 1 .. 10);
            |
         >>> duplication of aspect for "F" given at line 4

      6.    pragma Pre (A = 5);
            |
         >>> duplication of aspect for "F" given at line 4

      7.    pragma Post (Check => F'Result = 2);
                         |
         >>> pragma "Post" does not permit identifier "Check" here

      8.    pragma Post (F'Result = 1, "message");
                                       |
         >>> too many arguments for pragma "Post"

      9.
     10.    function Q (M : Integer) return Integer;
     11.    pragma Pre_Class (M > 5);
     12.    pragma Pre (M > 10);
     13.    pragma Post (Q'Result < 10);
     14.    pragma Post (Q'Result < 5);
            |
         >>> duplication of aspect for "Q" given at line 13

     15.
     16.    package Inner is
     17.       type R is tagged null record;
     18.       procedure Prim (Arg : R);
     19.       pragma Pre_Class (True);
     20.       pragma Pre (False);
     21.    end Inner;
     22.
     23.    package body Inner is
     24.       procedure Prim (Arg : R) is
     25.       begin
     26.          null;
     27.       end Prim;
     28.    end Inner;
     29.
     30.    function F (A : Integer) return Integer is
     31.       pragma Post (F'Result = 3);
               |
         >>> pragma "Post" must apply to subprogram specification

     32.    begin
     33.       return 2 * A;
     34.    end;
     35.    function F1 (A : Integer) return Integer is
     36.       pragma Post (F1'Result = 3); -- OK no spec
     37.    begin
     38.       return 2 * A;
     39.    end;
     40.    function Q (M : Integer) return Integer is
     41.    begin
     42.       return 42;
     43.    end;
     44. begin
     45.    null;
     46. end PostPrePragE;

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

2013-10-13  Robert Dewar  <dewar@adacore.com>

	* gnat_rm.texi: Add documentation for pragmas Pre[_Class]
	Post[_Class].
	* par-ch2.adb (Skip_Pragma_Semicolon): Handle extra semicolon nicely.
	* par-prag.adb: Add entries for pragmas Pre[_Class] and
	Post[_Class].
	* sem_prag.adb: Add handling of pragmas Pre[_Class] and
	Post[_Class].
	* sem_util.adb (Original_Aspect_Name): Moved here from
	Sem_Prag.Original_Name, and modified to handle pragmas
	Pre/Post/Pre_Class/Post_Class.
	* sem_util.ads (Original_Aspect_Name): Moved here from
	Sem_Prag.Original_Name.
	* snames.ads-tmpl: Add entries for pragmas Pre[_Class] and
	Post[_Class].

[Ada] Implement new pragmas Pre[_Class] and Post[_Class]

Commit Message

Patch