diff options
Diffstat (limited to 'gcc/ada/doc')
8 files changed, 139 insertions, 48 deletions
diff --git a/gcc/ada/doc/gnat_rm/gnat_language_extensions.rst b/gcc/ada/doc/gnat_rm/gnat_language_extensions.rst index ed534d1..f80ea52 100644 --- a/gcc/ada/doc/gnat_rm/gnat_language_extensions.rst +++ b/gcc/ada/doc/gnat_rm/gnat_language_extensions.rst @@ -581,30 +581,6 @@ Restricting the position of controlling parameter offers several advantages: * The result of a function is never a controlling result. -``Unsigned_Base_Range`` aspect ------------------------------- - -A new pragma/aspect, ``Unsigned_Base_Range``, is introduced to explicitly -enforce the use of an unsigned base type for signed integer types. -RM-3.5.4(9) mandates a symmetric base range for signed integer types. This -requirement often requires the use of larger data types for arithmetic -operations, potentially introducing undesirable run-time overhead and -performance penalties, particularly in embedded systems. For instance, -on a 64-bit architecture, a 64-bit multiplication can be performed with -a single hardware instruction, whereas a 128-bit multiplication requires -multiple instructions and intermediate steps. - -Here is an example of this feature: - -.. code-block:: ada - - type Uns_64 is range 0 .. 2 ** 64 - 1 - with Size => 64, - Unsigned_Base_Range => True; - -It ensures that arithmetic operations of type ``Uns_64`` are carried -out using 64 bits. - Generalized Finalization ------------------------ diff --git a/gcc/ada/doc/gnat_rm/implementation_advice.rst b/gcc/ada/doc/gnat_rm/implementation_advice.rst index d4fdd09..7eccbbc 100644 --- a/gcc/ada/doc/gnat_rm/implementation_advice.rst +++ b/gcc/ada/doc/gnat_rm/implementation_advice.rst @@ -1218,7 +1218,8 @@ RM E.5(28-29): Partition Communication Subsystem should allow them to block until the corresponding subprogram body returns." -A separately supplied PCS that can be used with GNAT when combined with the PolyORB product. +A separately supplied PCS that can be used with GNAT when combined with the PolyORB product (NB! See the note in :ref:`polyORB` regarding the lifetime +of this product). "The ``Write`` operation on a stream of type ``Params_Stream_Type`` should raise ``Storage_Error`` if it runs out of space trying to diff --git a/gcc/ada/doc/gnat_rm/implementation_defined_characteristics.rst b/gcc/ada/doc/gnat_rm/implementation_defined_characteristics.rst index f7746c8..887cc11 100644 --- a/gcc/ada/doc/gnat_rm/implementation_defined_characteristics.rst +++ b/gcc/ada/doc/gnat_rm/implementation_defined_characteristics.rst @@ -377,7 +377,8 @@ may have been set by a call to ``Ada.Command_Line.Set_Exit_Status``). * "The mechanisms for building and running partitions. See 10.2(24)." -GNAT itself supports programs with only a single partition. The PolyORB product (which also includes an implementation of the PCS) provides a completely flexible method for building and running programs consisting of multiple partitions. See the separate PolyORB user guide for details. +GNAT itself supports programs with only a single partition. The PolyORB product (which also includes an implementation of the PCS) provides a completely flexible method for building and running programs consisting of multiple partitions. **NB!** See the note in :ref:`polyORB` regarding the lifetime +of this product. * "The details of program execution, including program @@ -390,8 +391,7 @@ See separate section on compilation model. implementation. See 10.2(28)." Passive partitions are supported on targets where shared memory is -provided by the operating system. See the PolyORB user guide for -further details. +provided by the operating system. **NB!** See the note in :ref:`polyORB` regarding the lifetime of this product. * "The information returned by ``Exception_Message``. See 11.4.1(10)." @@ -1185,27 +1185,29 @@ Unknown. programs. See E(5)." The PolyORB product provides means creating and executing -distributed programs. See the PolyORB user guide for further details. +distributed programs. **NB!** See the note in :ref:`polyORB` regarding the lifetime of this product. * "Any events that can result in a partition becoming inaccessible. See E.1(7)." See the PolyORB user guide for full details on such events. +**NB!** Consider the note in :ref:`polyORB` regarding the lifetime +of this product. * "The scheduling policies, treatment of priorities, and management of shared resources between partitions in certain cases. See E.1(11)." See the PolyORB user guide for full details on these aspects of -multi-partition execution. +multi-partition execution. **NB!** Consider the note in :ref:`polyORB` regarding the lifetime of this product. * "Whether the execution of the remote subprogram is immediately aborted as a result of cancellation. See E.4(13)." See the PolyORB user guide for details on the effect of abort in -a distributed application. +a distributed application. **NB!** Consider the note in :ref:`polyORB` regarding the lifetime of this product. * "The range of type System.RPC.Partition_Id. See E.5(14)." @@ -1216,7 +1218,7 @@ System.RPC.Partition_ID'Last is Integer'Last. See source file :file:`s-rpc.ads`. "Implementation-defined interfaces in the PCS. See E.5(26)." See the PolyORB user guide for a full description of all -implementation defined interfaces. +implementation defined interfaces. **NB!** See the note in :ref:`polyORB` regarding the lifetime of this product. * "The values of named numbers in the package diff --git a/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst b/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst index 3986298..183b2ff 100644 --- a/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst +++ b/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst @@ -398,9 +398,8 @@ The analyzed pragma is retained in the tree, but not otherwise processed by any part of the GNAT compiler, except to generate corresponding note lines in the generated ALI file. For the format of these note lines, see the compiler source file lib-writ.ads. This pragma is intended for use by -external tools, including ASIS. The use of pragma Annotate does not -affect the compilation process in any way. This pragma may be used as -a configuration pragma. +external tools. The use of pragma Annotate does not affect the compilation +process in any way. This pragma may be used as a configuration pragma. Pragma Assert ============= @@ -466,6 +465,10 @@ of Ada from 2005 on. In GNAT, it is implemented in all versions of Ada, and the DISABLE policy is an implementation-defined addition. +This is an assertion kind pragma that can associate a set of its arguments +with an assertion level. See SPARK 2014 Reference Manual, section +11.4.2. + Pragma Assert_And_Cut ===================== @@ -490,6 +493,25 @@ a subprogram into sections for the purposes of testing or formal verification. The pragma also serves as useful documentation. +This is an assertion kind pragma that can associate a set of its arguments +with an assertion level. See SPARK 2014 Reference Manual, section +11.4.2. + +Pragma Assertion_Level +======================= + +Syntax:: + + pragma Assertion_Level (LEVEL_IDENTIFIER + [, depends => DEPENDENCY_DESCRIPTOR]); + + DEPENDENCY_DESCRIPTOR ::= LEVEL_IDENTIFIER | LEVEL_IDENTIFIER_LIST + + LEVEL_IDENTIFIER_LIST ::= '[' LEVEL_IDENTIFIER {, LEVEL_IDENTIFIER} ']' + +For the semantics of this pragma, see the SPARK 2014 Reference Manual, +section 11.4.3. + Pragma Assertion_Policy ======================= @@ -501,7 +523,7 @@ Syntax:: ASSERTION_KIND => POLICY_IDENTIFIER {, ASSERTION_KIND => POLICY_IDENTIFIER}); - ASSERTION_KIND ::= RM_ASSERTION_KIND | ID_ASSERTION_KIND + ASSERTION_KIND ::= RM_ASSERTION_KIND | ID_ASSERTION_KIND | ASSERTION_LEVEL RM_ASSERTION_KIND ::= Assert | Static_Predicate | @@ -541,6 +563,10 @@ The assertion kinds ``RM_ASSERTION_KIND`` are those defined in the Ada standard. The assertion kinds ``ID_ASSERTION_KIND`` are implementation defined additions recognized by the GNAT compiler. +Additionally the pragma can apply to an assertion level defined by the +``Assertion_Level`` pragma. For more details see the SPARK 2014 Reference +Manual, section 11.4.2. + The pragma applies in both cases to pragmas and aspects with matching names, e.g. ``Pre`` applies to the Pre aspect, and ``Precondition`` applies to both the ``Precondition`` pragma @@ -608,6 +634,10 @@ but it acts as a useful run-time check that the assumption is met, and documents the need to ensure that it is met by reference to information outside the program. +This is an assertion kind pragma that can associate a set of its arguments +with an assertion level. See SPARK 2014 Reference Manual, section +11.4.2. + Pragma Assume_No_Invalid_Values =============================== .. index:: Invalid representations @@ -1297,6 +1327,10 @@ call, as determined by the corresponding case guard evaluating to True, and that the consequence for this case should hold when the subprogram returns. +This is an assertion kind pragma that can associate a set of its arguments +with an assertion level. See SPARK 2014 Reference Manual, section +11.4.2. + Pragma Convention_Identifier ============================ .. index:: Conventions, synonyms @@ -1505,6 +1539,10 @@ pragmas can be enabled either by use of the command line switch *-gnata* or by use of the pragma ``Check_Policy`` with a first argument of ``Debug``. +This is an assertion kind pragma that can associate a set of its arguments +with an assertion level. See SPARK 2014 Reference Manual, section +11.4.2. + Pragma Debug_Policy =================== @@ -1534,6 +1572,10 @@ Syntax: For the semantics of this pragma, see the entry for aspect ``Default_Initial_Condition`` in the SPARK 2014 Reference Manual, section 7.3.3. +This is an assertion kind pragma that can associate a set of its arguments +with an assertion level. See SPARK 2014 Reference Manual, section +11.4.2. + Pragma Default_Scalar_Storage_Order =================================== .. index:: Default_Scalar_Storage_Order @@ -2922,6 +2964,10 @@ Syntax: For the semantics of this pragma, see the entry for aspect ``Initial_Condition`` in the SPARK 2014 Reference Manual, section 7.1.6. +This is an assertion kind pragma that can associate a set of its arguments +with an assertion level. See SPARK 2014 Reference Manual, section +11.4.2. + Pragma Initialize_Scalars ========================= .. index:: debugging with Initialize_Scalars @@ -3274,6 +3320,10 @@ invariant pragma for the same entity. For further details on the use of this pragma, see the Ada 2012 documentation of the Type_Invariant aspect. +This is an assertion kind pragma that can associate a set of its arguments +with an assertion level. See SPARK 2014 Reference Manual, section +11.4.2. + Pragma Keep_Names ================= @@ -3651,6 +3701,10 @@ may be used to refer to the value of an expression on entry to the loop. This attribute can only be used within the expression of a ``Loop_Invariant`` pragma. For full details, see documentation of attribute ``Loop_Entry``. +This is an assertion kind pragma that can associate a set of its arguments +with an assertion level. See SPARK 2014 Reference Manual, section +11.4.2. + Pragma Loop_Optimize ==================== @@ -3753,6 +3807,10 @@ statements. The ``Loop_Entry`` attribute may be used within the expressions of the ``Loop_Variant`` pragma to refer to values on entry to the loop. +This is an assertion kind pragma that can associate a set of its arguments +with an assertion level. See SPARK 2014 Reference Manual, section +11.4.2. + Pragma Machine_Attribute ======================== @@ -4627,6 +4685,10 @@ if there is no separate subprogram declaration, then it can appear at the start of the declarations in a subprogram body (preceded only by other pragmas). +This is an assertion kind pragma that can associate a set of its arguments +with an assertion level. See SPARK 2014 Reference Manual, section +11.4.2. + Pragma Postcondition ==================== .. index:: Postcondition @@ -4799,6 +4861,10 @@ use of the pragma identifier ``Check``. Historically, pragma Ada 2012, and has been retained in its original form for compatibility purposes. +This is an assertion kind pragma that can associate a set of its arguments +with an assertion level. See SPARK 2014 Reference Manual, section +11.4.2. + Pragma Post_Class ================= .. index:: Post @@ -4833,6 +4899,10 @@ aspects, but is prepared to ignore the pragmas. The assertion policy that controls this pragma is ``Post'Class``, not ``Post_Class``. +This is an assertion kind pragma that can associate a set of its arguments +with an assertion level. See SPARK 2014 Reference Manual, section +11.4.2. + Pragma Pre ========== .. index:: Pre @@ -4857,6 +4927,10 @@ if there is no separate subprogram declaration, then it can appear at the start of the declarations in a subprogram body (preceded only by other pragmas). +This is an assertion kind pragma that can associate a set of its arguments +with an assertion level. See SPARK 2014 Reference Manual, section +11.4.2. + Pragma Precondition =================== .. index:: Preconditions @@ -4917,6 +4991,10 @@ use of the pragma identifier ``Check``. Historically, pragma Ada 2012, and has been retained in its original form for compatibility purposes. +This is an assertion kind pragma that can associate a set of its arguments +with an assertion level. See SPARK 2014 Reference Manual, section +11.4.2. + .. _Pragma-Predicate: Pragma Predicate @@ -4977,6 +5055,10 @@ fundamentally changed (for example a membership test defined for subtype B). When following this approach, the use of predicates should be avoided. +This is an assertion kind pragma that can associate a set of its arguments +with an assertion level. See SPARK 2014 Reference Manual, section +11.4.2. + Pragma Predicate_Failure ======================== @@ -5074,6 +5156,10 @@ aspects, but is prepared to ignore the pragmas. The assertion policy that controls this pragma is ``Pre'Class``, not ``Pre_Class``. +This is an assertion kind pragma that can associate a set of its arguments +with an assertion level. See SPARK 2014 Reference Manual, section +11.4.2. + Pragma Priority_Specific_Dispatching ==================================== @@ -5562,6 +5648,10 @@ Syntax: For the semantics of this pragma, see the entry for aspect ``Refined_Post`` in the SPARK 2014 Reference Manual, section 7.2.7. +This is an assertion kind pragma that can associate a set of its arguments +with an assertion level. See SPARK 2014 Reference Manual, section +11.4.2. + .. _Pragma-Refined_State: Pragma Refined_State @@ -6547,6 +6637,9 @@ The ``Subprogram_Variant`` pragma is intended to be an exact replacement for the implementation-defined ``Subprogram_Variant`` aspect, and shares its restrictions and semantics. +This is an assertion kind pragma that can associate a set of its arguments +with an assertion level. See SPARK 2014 Reference Manual, section +11.4.2. Pragma Subtitle =============== @@ -6975,6 +7068,10 @@ does not permit a string parameter, and it is controlled by the assertion identifier ``Type_Invariant`` rather than ``Invariant``. +This is an assertion kind pragma that can associate a set of its arguments +with an assertion level. See SPARK 2014 Reference Manual, section +11.4.2. + .. _Pragma-Type_Invariant_Class: Pragma Type_Invariant_Class @@ -7004,6 +7101,10 @@ aspects, but is prepared to ignore the pragmas. The assertion policy that controls this pragma is ``Type_Invariant'Class``, not ``Type_Invariant_Class``. +This is an assertion kind pragma that can associate a set of its arguments +with an assertion level. See SPARK 2014 Reference Manual, section +11.4.2. + Pragma Unchecked_Union ====================== .. index:: Unions in C diff --git a/gcc/ada/doc/gnat_rm/obsolescent_features.rst b/gcc/ada/doc/gnat_rm/obsolescent_features.rst index 3ba5021..d78d986f 100644 --- a/gcc/ada/doc/gnat_rm/obsolescent_features.rst +++ b/gcc/ada/doc/gnat_rm/obsolescent_features.rst @@ -5,9 +5,19 @@ Obsolescent Features ******************** This chapter describes features that are provided by GNAT, but are -considered obsolescent since there are preferred ways of achieving -the same effect. These features are provided solely for historical -compatibility purposes. +considered obsolescent since there are other, more appropriate, ways +of achieving the same effect. These features are provided solely for +historical compatibility purposes. + +.. _polyORB: + +PolyORB +======== + +AWS is a deprecated product. It will be baselined with the GNAT Pro +release 28. After this release, there will be no new versions of this +product. Contact your sales representative or send a message to +sales@adacore.com to get recommendations for replacements. .. _pragma_No_Run_Time: diff --git a/gcc/ada/doc/gnat_rm/specialized_needs_annexes.rst b/gcc/ada/doc/gnat_rm/specialized_needs_annexes.rst index f34368c..666e0b3 100644 --- a/gcc/ada/doc/gnat_rm/specialized_needs_annexes.rst +++ b/gcc/ada/doc/gnat_rm/specialized_needs_annexes.rst @@ -17,7 +17,7 @@ Ada 95, Ada 2005, Ada 2012, and Ada 2022 define a number of Specialized Needs An *Distributed Systems (Annex E)* Stub generation is fully implemented in the GNAT compiler. In addition, a complete compatible PCS is available as part of ``PolyORB``, - a separate product. Note, that PolyORB is a deprecated product and will be eventually replaced with other technologies such as ``RTI``. + a separate product. **NB!** See the note in :ref:`polyORB` regarding the lifetime of this product. *Information Systems (Annex F)* diff --git a/gcc/ada/doc/gnat_rm/the_gnat_library.rst b/gcc/ada/doc/gnat_rm/the_gnat_library.rst index 29642aa..bd17490 100644 --- a/gcc/ada/doc/gnat_rm/the_gnat_library.rst +++ b/gcc/ada/doc/gnat_rm/the_gnat_library.rst @@ -2047,7 +2047,8 @@ technically an implementation-defined addition). This package provides facilities for partition interfacing. It is used primarily in a distribution context when using Annex E -with ``PolyORB``. +with ``PolyORB``. **NB!** See the note in :ref:`polyORB` regarding +the lifetime of this product. .. _`System.Pool_Global_(s-pooglo.ads)`: 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 b46f69b..80f81a8 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 @@ -1937,13 +1937,13 @@ Alphabetical List of All Switches Ignore representation clauses. When this switch is used, representation clauses are treated as comments. This is useful when initially porting code where you want to ignore rep clause - problems, and also for compiling foreign code (particularly - for use with ASIS). The representation clauses that are ignored - are: enumeration_representation_clause, record_representation_clause, - and attribute_definition_clause for the following attributes: - Address, Alignment, Bit_Order, Component_Size, Machine_Radix, - Object_Size, Scalar_Storage_Order, Size, Small, Stream_Size, - and Value_Size. Pragma Default_Scalar_Storage_Order is also ignored. + problems, and also for compiling foreign code. The representation + clauses that are ignored are: enumeration_representation_clause, + record_representation_clause, and attribute_definition_clause for the + following attributes: Address, Alignment, Bit_Order, Component_Size, + Machine_Radix, Object_Size, Scalar_Storage_Order, Size, Small, + Stream_Size, and Value_Size. + Pragma Default_Scalar_Storage_Order is also ignored. Note that this option should be used only for compiling -- the code is likely to malfunction at run time. |