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

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

[Pierre-Marie de Rodat]

https://gcc.gnu.org/g:82b63eb0f30333b3c59e8f37c4007cb6fd3fe0f9

commit r13-1425-g82b63eb0f30333b3c59e8f37c4007cb6fd3fe0f9
Author: Claire Dross <dross@adacore.com>
Date:   Tue May 24 10:42:46 2022 +0200

    [Ada] Add GNAT specific pragmas to the equivalent Assertion_Policy for -gnata
    
    All assertion pragmas are enabled by default when using -gnata. We need
    to add the GNAT specific ones to the list.
    
    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.

Diff:
---
 .../building_executable_programs_with_gnat.rst     | 34 ++++++++++++++-----
 gcc/ada/gnat_ugn.texi                              | 38 +++++++++++++++-------
 2 files changed, 52 insertions(+), 20 deletions(-)

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
index 29293e1f847..2e835f2f353 100644
--- 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
index a2a2990b6d7..a080cd43871 100644
--- 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