[Ada] Implement Ada 2012 Assertion_Policy pragma

This implements pragma Assertion_Policy as described in AI 274. The
main improvements are that it can appear in any declarative part
with scope rules like pragma Suppress, and it can be applied to
individual assertion aspects. GNAT extensions allow it to also
apply to GNAT assertion aspects and pragmas. Check_Policy is
enhanced in a consistent manner. Finally Debug pragmas are
now controllable with Assertion_Policy.

The following program generates:

OK 1
OK 3
OK 4
OK 5
OK 6
OK 7

if compiled with out -gnata, and

OK 1
OK 2
OK 3
OK 4
OK 5
OK 6
OK 7

if compiled with -gnata

     1. pragma Ada_2012;
     2. with Text_IO; use Text_IO;
     3. with System.Assertions; use System.Assertions;
     4. procedure TestPolicy is
     5.    function Ident (M : Integer) return Integer is
     6.    begin return M; end;
     7. begin
     8.    begin
     9.       declare
    10.          pragma Check_Policy (Debug, Check);
    11.          pragma Debug (True, Put_Line ("OK 1"));
    12.          pragma Check_Policy (Debug, Ignore);
    13.          pragma Debug (True, Put_Line ("Not OK 1"));
    14.          pragma Check_Policy (Debug, Disable);
    15.          pragma Debug (True, 32);
    16.       begin
    17.          null;
    18.       end;
    19.
    20.       pragma Debug (True, Put_Line ("OK 2"));
    21.       null;
    22.    end;
    23.
    24.    declare
    25.       pragma Assertion_Policy (Pre => Disable);
    26.       procedure P1 with Pre => 32 is begin null; end;
    27.    begin
    28.       P1;
    29.    end;
    30.
    31.    declare
    32.       pragma Assertion_Policy (Pre => Check);
    33.       procedure P1 with Pre => False is begin null; end;
    34.    begin
    35.       P1;
    36.    exception
    37.       when Assert_Failure => Put_Line ("OK 3");
    38.    end;
    39.
    40.    declare
    41.       pragma Assertion_Policy (Pre => Ignore);
    42.       procedure P1 with Pre => False is begin null; end;
    43.    begin
    44.       P1;
    45.    exception
    46.       when Assert_Failure => Put_Line ("Not OK 2");
    47.    end;
    48.
    49.    begin
    50.       null;
    51.    end;
    52.
    53.    declare
    54.       pragma Assertion_Policy (Post => Check);
    55.       procedure P1 with Post => False is begin null; end;
    56.    begin
    57.       P1;
    58.    exception
    59.       when Assert_Failure => Put_Line ("OK 4");
    60.    end;
    61.
    62.    declare
    63.       pragma Assertion_Policy (Post => Ignore);
    64.       procedure P1 with Post => False is begin null; end;
    65.    begin
    66.       P1;
    67.    exception
    68.       when Assert_Failure => Put_Line ("Not OK 3");
    69.    end;
    70.
    71.    declare
    72.       pragma Assertion_Policy (Static_Predicate => Check);
    73.       subtype X is Integer with Static_Predicate => X > 0;
    74.       XX : X;
    75.    begin
    76.       XX := Ident (-4);
    77.    exception
    78.       when Assert_Failure => Put_Line ("OK 5");
    79.    end;
    80.
    81.    declare
    82.       pragma Check_Policy (Static_Predicate, Ignore);
    83.       subtype X is Integer with Static_Predicate => X > 0;
    84.       XX : X;
    85.    begin
    86.       XX := Ident (-4);
    87.    exception
    88.       when Assert_Failure => Put_Line ("Not OK 4");
    89.    end;
    90.
    91.    declare
    92.       pragma Assertion_Policy (Dynamic_Predicate => Check);
    93.       subtype X is Integer with Dynamic_Predicate => X > Ident (0);
    94.       XX : X;
    95.    begin
    96.       XX := Ident (-4);
    97.    exception
    98.       when Assert_Failure => Put_Line ("OK 6");
    99.    end;
   100.
   101.    declare
   102.       pragma Assertion_Policy (Dynamic_Predicate => Ignore);
   103.       subtype X is Integer with Dynamic_Predicate => X > Ident (0);
   104.       XX : X;
   105.    begin
   106.       XX := Ident (-4);
   107.    exception
   108.       when Assert_Failure => Put_Line ("Not OK 6");
   109.    end;
   110.
   111.    declare
   112.       pragma Check_Policy (Predicate, Check);
   113.       subtype X is Integer with Predicate => X > 0;
   114.       XX : X;
   115.    begin
   116.       XX := Ident (-4);
   117.    exception
   118.       when Assert_Failure => Put_Line ("OK 7");
   119.    end;
   120.
   121.    declare
   122.       pragma Assertion_Policy (Predicate => Ignore);
   123.       subtype X is Integer with Predicate => X > 0;
   124.       XX : X;
   125.    begin
   126.       XX := Ident (-4);
   127.    exception
   128.       when Assert_Failure => Put_Line ("Not OK 6");
   129.    end;
   130.
   131. end;

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

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

	* einfo.adb (Has_Dynamic_Predicate_Aspect): New flag.
	(Has_Static_Predicate_Aspect): New flag.
	* einfo.ads (Has_Dynamic_Predicate_Aspect): New flag.
	(Has_Static_Predicate_Aspect): New flag.
	* exp_ch9.adb: Minor reformatting.
	* exp_util.adb (Make_Invariant_Call): Check_Enabled now handles
	synonyms.
	* gnat1drv.adb: Remove setting of Debug_Pragmas_Enabled,
	since this switch is gone and control of Debug is done with
	Assertions_Enabled.
	* gnat_rm.texi: Update documentation for Assertion_Policy and
	Check_Policy pragmas.
	* opt.adb (Debug_Pragmas_Disabled[_Config]): Removed
	(Debug_Pragmas_Enabled[_Config]): Removed Since debug now
	controlled by Assertion_Enabled.
	* opt.ads (Debug_Pragmas_Disabled[_Config]): Removed
	(Debug_Pragmas_Enabled[_Config]): Removed Since debug now
	controlled by Assertion_Enabled.
	* par-ch2.adb (Scan_Pragma_Argument_Association): Allow new
	'Class forms.
	* sem_attr.adb: Minor reformatting.
	* sem_ch13.adb (Analyze_Aspect_Specification): Disable aspect
	if DISABLE policy applies.
	* sem_ch6.adb (Grab_PPC): Check original name of aspect for
	aspect from pragma (Process_PPCs): Properly check assertion policy.
	* sem_prag.adb (Check_Enabled): Rewritten for new Assertion_Policy
	(Check_Appicable_Policy): New procedure.
	(Is_Valid_Assertion_Kind): New function.
	(Rewrite_Assertion_Kind): New procedure.
	(Analyze_Pragma): Handle case of disabled assertion pragma.
	(Analyze_Pragma, case Assertion_Policy): Rewritten for Ada 2012.
	(Analyze_Pragma, case Check): Deal with 'Class possibilities.
	(Analyze_Pragma, case Check_Policy): Deal with 'Class possibilities.
	(Analyze_Pragma, case Contract_Class): New handling of ignored pragma.
	(Analyze_Pragma, case Debug): New control with Assertion_Policy.
	(Analyze_Pragma, case Debug_Policy): Now consistent with
	Assertion_Policy.
	(Analyze_Pragma, case Loop_Invariant): New handling of ignored
	pragma.
	(Analyze_Pragma, case Loop_Variant): New handling of ignored pragma.
	(Analyze_Pragma, case Precondition): Use proper name for Check pragma.
	(Analyze_Pragma, case Check_Enabled): Rewritten for new policy stuff.
	* sem_prag.ads (Check_Enabled): Rewritten for new
	Assertion_Policy stuff.
	(Check_Appicable_Policy): New procedure.
	* sinfo.adb (Is_Disabled): New flag.
	(Is_Ignored): New flag.
	* sinfo.ads (Is_Disabled): New flag.
	(Is_Ignored): New flag.
	(N_Pragma_Argument_Association): New 'Class forms.
	* snames.ads-tmpl: New names Name_uPre, Name_uPost,
	Name_uType_Invariant, Name_uInvariant.
	* switch-c.adb: Remove setting of Debug_Pragmas_Enabled for -gnata.
	* tree_io.ads (ASIS_Version_Number): Updated (remove
	read write of obsolete flags Debug_Pragmas_Disabled and
	Debug_Pragmas_Enabled.

[Ada] Implement Ada 2012 Assertion_Policy pragma

Commit Message

Patch