diff options
Diffstat (limited to 'gcc/ada/doc')
| -rw-r--r-- | gcc/ada/doc/gnat_rm/implementation_defined_aspects.rst | 7 | ||||
| -rw-r--r-- | gcc/ada/doc/gnat_rm/implementation_defined_attributes.rst | 8 |
2 files changed, 14 insertions, 1 deletions
diff --git a/gcc/ada/doc/gnat_rm/implementation_defined_aspects.rst b/gcc/ada/doc/gnat_rm/implementation_defined_aspects.rst index 89f6718..736710d 100644 --- a/gcc/ada/doc/gnat_rm/implementation_defined_aspects.rst +++ b/gcc/ada/doc/gnat_rm/implementation_defined_aspects.rst @@ -464,6 +464,13 @@ Aspect Refined_State This aspect is equivalent to :ref:`pragma Refined_State<Pragma-Refined_State>`. +Aspect Relaxed_Initialization +============================= +.. index:: Refined_Initialization + +For the syntax and semantics of this aspect, see the SPARK 2014 Reference +Manual, section 6.10. + Aspect Remote_Access_Type ========================= .. index:: Remote_Access_Type diff --git a/gcc/ada/doc/gnat_rm/implementation_defined_attributes.rst b/gcc/ada/doc/gnat_rm/implementation_defined_attributes.rst index cfde81e..967e9d9 100644 --- a/gcc/ada/doc/gnat_rm/implementation_defined_attributes.rst +++ b/gcc/ada/doc/gnat_rm/implementation_defined_attributes.rst @@ -511,6 +511,13 @@ that returns the appropriate string when called. This means that ``X'Img`` can be renamed as a function-returning-string, or used in an instantiation as a function parameter. +Attribute Initialized +===================== +.. index:: Initialized + +For the syntax and semantics of this attribute, see the SPARK 2014 Reference +Manual, section 6.10. + Attribute Integer_Value ======================= .. index:: Integer_Value @@ -1616,4 +1623,3 @@ Attribute Word_Size ``Standard'Word_Size`` (``Standard`` is the only permissible prefix) provides the value ``System.Word_Size``. The result is a static constant. - |