[Ada] Implement new assertion kind Statement_Assertions

[Arnaud Charlet <charlet at adacore dot com>]

This patch implements a new assertion kind (usable in a Check_Policy
or Assertion_Policy pragma) "Statement_Assertions" which applies to
Assert, Assert_And_Cut, Assume, and Loop_Invariant.

The following program is to be compiled with the -gnatd.F switch (this
switch can be removed soon when we make the other assertion kinds first
class citizens)

     1. pragma Ada_2012;
     2. with Text_IO; use Text_IO;
     3. with System.Assertions; use System.Assertions;
     4. procedure StmAssert is
     5.    function Id (X : Integer) return Integer
     6.    is begin return X; end;
     7.
     8.    Y : Integer := Id (10);
     9.
    10. begin
    11.    declare
    12.       pragma Check_Policy
    13.         (Statement_Assertions, Check);
    14.    begin
    15.       begin
    16.          pragma Assert (Y = 11);
    17.          Put_Line ("not OK1");
    18.       exception
    19.          when Assert_Failure =>
    20.             Put_Line ("OK1");
    21.       end;
    22.       begin
    23.          pragma Assert_And_Cut (Y = 11);
    24.          Put_Line ("not OK2");
    25.       exception
    26.          when Assert_Failure =>
    27.             Put_Line ("OK2");
    28.       end;
    29.       begin
    30.          pragma Assume (Y = 11);
    31.          Put_Line ("not OK3");
    32.       exception
    33.          when Assert_Failure =>
    34.             Put_Line ("OK3");
    35.       end;
    36.       begin
    37.          for J in 1 .. 1 loop
    38.             pragma Loop_Invariant (Y = 11);
    39.             Put_Line ("not OK4");
    40.          end loop;
    41.       exception
    42.          when Assert_Failure =>
    43.             Put_Line ("OK4");
    44.       end;
    45.    end;
    46.    declare
    47.       pragma Assertion_Policy
    48.         (Statement_Assertions => Ignore);
    49.    begin
    50.       pragma Assert (Y = 11);
    51.       pragma Assert_And_Cut (Y = 11);
    52.       pragma Assume (Y = 11);
    53.       for J in 1 .. 1 loop
    54.          pragma Loop_Invariant (J = 2);
    55.       end loop;
    56.       Put_Line ("OK5");
    57.    exception
    58.       when others => Put_Line ("not OK5");
    59.    end;
    60.
    61. end StmAssert;

The output is:

OK1
OK2
OK3
OK4
OK5

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

2013-04-23  Robert Dewar  <dewar@adacore.com>

	* exp_prag.adb (Expand_Pragma_Check): Check for Assert rather
	than Assertion.
	* sem_prag.adb (Is_Valid_Assertion_Kind): Moved to spec
	(Effective_Name): New function (Analyze_Pragma, case Check):
	Disallow [Statement_]Assertions (Check_Kind): Implement
	Statement_Assertions (Check_Applicable_Policy): Use Effective_Name
	(Is_Valid_Assertion_Kind): Allow Statement_Assertions.
	* sem_prag.ads (Is_Valid_Assertion_Kind): Moved here from body
	(Effective_Name): New function.
	* sem_res.adb: Minor reformatting.
	* snames.ads-tmpl (Name_Statement_Assertions): New entry.
	* gnat_rm.texi: Add documentation of new assertion kind
	Statement_Assertions.

Attachment: difs
Description: Text document