procyberian/gcc
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

ada: Add documentation for Exceptional_Cases

Browse source 
Add minimal description for pragma and aspect Exceptional_Cases, based
on a similarly minimal descriptions for other SPARK contracts.

gcc/ada/
	* doc/gnat_rm/implementation_defined_aspects.rst
	(Exceptional_Cases): Add description for aspect.
	* doc/gnat_rm/implementation_defined_pragmas.rst
	(Exceptional_Cases): Add description for pragma.
	* gnat_rm.texi: Regenerate.
	* gnat_ugn.texi: Regenerate.
This commit is contained in:
Piotr Trojanek 2024-01-23 16:42:30 +01:00 • committed by Marc Poulhiès
parent 18e881ebd9
commit ab5bb2bc3f
4 changed files with 876 additions and 807 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
gcc/ada/doc/gnat_rm/implementation_defined_aspects.rst
View file

@ -243,6 +243,18 @@ Aspect Effective_Writes
This aspect is equivalent to :ref:`pragma Effective_Writes<Pragma-Effective_Writes>`.
Aspect Exceptional_Cases
========================
.. index:: Exceptional_Cases
This aspect may be specified for procedures and functions with side effects;
it can be used to list exceptions that might be propagated by the subprogram
with side effects in the context of its precondition, and associate them
with a specific postcondition.
For the syntax and semantics of this aspect, see the SPARK 2014 Reference
Manual, section 6.1.9.
Aspect Extensions_Visible
=========================
.. index:: Extensions_Visible

18
gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
View file

@ -1919,6 +1919,24 @@ configuration pragma, or in a declaration sequence where it applies
till the end of the scope. If an ``Entity`` argument is present,
the action applies only to that entity.
Pragma Exceptional_Cases
========================
.. index:: Exceptional_Cases
Syntax:
::
pragma Exceptional_Cases (EXCEPTIONAL_CASE_LIST);
EXCEPTIONAL_CASE_LIST ::= EXCEPTIONAL_CASE {, EXCEPTIONAL_CASE}
EXCEPTIONAL_CASE ::= exception_choice {'|' exception_choice} => CONSEQUENCE
CONSEQUENCE ::= Boolean_expression
For the semantics of this aspect, see the SPARK 2014 Reference Manual, section
6.1.9.
Pragma Export_Function
======================
.. index:: Argument passing mechanisms

1649
gcc/ada/gnat_rm.texi
View file

File diff suppressed because it is too large Load diff

4
gcc/ada/gnat_ugn.texi
View file

@ -19,7 +19,7 @@
@copying
@quotation
GNAT User's Guide for Native Platforms , Dec 21, 2023
GNAT User's Guide for Native Platforms , Apr 15, 2024
AdaCore
@ -29580,8 +29580,8 @@ to permit their use in free software.
@printindex ge
@anchor{d1}@w{ }
@anchor{gnat_ugn/gnat_utility_programs switches-related-to-project-files}@w{ }
@anchor{d1}@w{ }
@c %**end of body
@bye