[Ada] Add GNAT specific pragmas to the equivalent Assertion_Policy for -gnata

[Ada] Add GNAT specific pragmas to the equivalent Assertion_Policy for -gnata

[Pierre-Marie de Rodat]

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

All assertion pragmas are enabled by default when using -gnata. We need
to add the GNAT specific ones to the list.

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

gcc/ada/

	* doc/gnat_ugn/building_executable_programs_with_gnat.rst
	(Debugging and Assertion Control): Add GNAT specific assertion
	pragmas to the equivalent Assertion_Policy for the -gnata
	option.
	* gnat_ugn.texi: Regenerate.

[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 4223 bytes --]

diff --git a/gcc/ada/doc/gnat_ugn/building_executable_programs_with_gnat.rst b/gcc/ada/doc/gnat_ugn/building_executable_programs_with_gnat.rst
--- a/gcc/ada/doc/gnat_ugn/building_executable_programs_with_gnat.rst
+++ b/gcc/ada/doc/gnat_ugn/building_executable_programs_with_gnat.rst
@@ -4331,15 +4331,31 @@ Debugging and Assertion Control
   Which is a shorthand for::
 
        pragma Assertion_Policy
-         (Assert               => Check,
-          Static_Predicate     => Check,
-          Dynamic_Predicate    => Check,
-          Pre                  => Check,
-          Pre'Class            => Check,
-          Post                 => Check,
-          Post'Class           => Check,
-          Type_Invariant       => Check,
-          Type_Invariant'Class => Check);
+       --  Ada RM assertion pragmas
+         (Assert                    => Check,
+          Static_Predicate          => Check,
+          Dynamic_Predicate         => Check,
+          Pre                       => Check,
+          Pre'Class                 => Check,
+          Post                      => Check,
+          Post'Class                => Check,
+          Type_Invariant            => Check,
+          Type_Invariant'Class      => Check,
+          Default_Initial_Condition => Check,
+       --  GNAT specific assertion pragmas
+          Assert_And_Cut            => Check,
+          Assume                    => Check,
+          Contract_Cases            => Check,
+          Debug                     => Check,
+          Ghost                     => Check,
+          Initial_Condition         => Check,
+          Loop_Invariant            => Check,
+          Loop_Variant              => Check,
+          Postcondition             => Check,
+          Precondition              => Check,
+          Predicate                 => Check,
+          Refined_Post              => Check,
+          Subprogram_Variant        => Check);
 
   The pragmas ``Assert`` and ``Debug`` normally have no effect and
   are ignored. This switch, where ``a`` stands for 'assert', causes


diff --git a/gcc/ada/gnat_ugn.texi b/gcc/ada/gnat_ugn.texi
--- a/gcc/ada/gnat_ugn.texi
+++ b/gcc/ada/gnat_ugn.texi
@@ -21,7 +21,7 @@
 
 @copying
 @quotation
-GNAT User's Guide for Native Platforms , May 24, 2022
+GNAT User's Guide for Native Platforms , Jun 24, 2022
 
 AdaCore
 
@@ -12853,15 +12853,31 @@ Which is a shorthand for:
 
 @example
 pragma Assertion_Policy
-  (Assert               => Check,
-   Static_Predicate     => Check,
-   Dynamic_Predicate    => Check,
-   Pre                  => Check,
-   Pre'Class            => Check,
-   Post                 => Check,
-   Post'Class           => Check,
-   Type_Invariant       => Check,
-   Type_Invariant'Class => Check);
+--  Ada RM assertion pragmas
+  (Assert                    => Check,
+   Static_Predicate          => Check,
+   Dynamic_Predicate         => Check,
+   Pre                       => Check,
+   Pre'Class                 => Check,
+   Post                      => Check,
+   Post'Class                => Check,
+   Type_Invariant            => Check,
+   Type_Invariant'Class      => Check,
+   Default_Initial_Condition => Check,
+--  GNAT specific assertion pragmas
+   Assert_And_Cut            => Check,
+   Assume                    => Check,
+   Contract_Cases            => Check,
+   Debug                     => Check,
+   Ghost                     => Check,
+   Initial_Condition         => Check,
+   Loop_Invariant            => Check,
+   Loop_Variant              => Check,
+   Postcondition             => Check,
+   Precondition              => Check,
+   Predicate                 => Check,
+   Refined_Post              => Check,
+   Subprogram_Variant        => Check);
 @end example
 
 The pragmas @code{Assert} and @code{Debug} normally have no effect and
@@ -29249,8 +29265,8 @@ to permit their use in free software.
 
 @printindex ge
 
-@anchor{gnat_ugn/gnat_utility_programs switches-related-to-project-files}@w{                              }
 @anchor{cf}@w{                              }
+@anchor{gnat_ugn/gnat_utility_programs switches-related-to-project-files}@w{                              }
 
 @c %**end of body
 @bye