From 09d67391ff9fa5a74a2bf727a50b5199b736fdb0 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Tue, 29 Jul 2014 15:58:21 +0200 Subject: [PATCH] [multiple changes] 2014-07-29 Thomas Quinot * gnat_rm.texi: Document internal attributes used for PolyORB/DSA distributed stubs generation. * exp_ch3.adb: Minor reformatting. 2014-07-29 Yannick Moy * sinfo.ads: Document constraint between frontend and GNATprove. From-SVN: r213193 --- gcc/ada/ChangeLog | 10 ++++++++++ gcc/ada/exp_ch3.adb | 2 +- gcc/ada/gnat_rm.texi | 26 ++++++++++++++++++++------ gcc/ada/sinfo.ads | 18 +++++++++++++----- 4 files changed, 44 insertions(+), 12 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 8966d9ea8a8..3354841e9dd 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,13 @@ +2014-07-29 Thomas Quinot + + * gnat_rm.texi: Document internal attributes used for PolyORB/DSA + distributed stubs generation. + * exp_ch3.adb: Minor reformatting. + +2014-07-29 Yannick Moy + + * sinfo.ads: Document constraint between frontend and GNATprove. + 2014-07-29 Robert Dewar * a-except.adb: Minor comment clarification. diff --git a/gcc/ada/exp_ch3.adb b/gcc/ada/exp_ch3.adb index 5a6b0f9918b..f18f255aed2 100644 --- a/gcc/ada/exp_ch3.adb +++ b/gcc/ada/exp_ch3.adb @@ -3173,7 +3173,7 @@ package body Exp_Ch3 is exception when RE_Not_Available => - return Empty_List; + return Empty_List; end Build_Init_Statements; ------------------------- diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi index 0f48f495004..9b5e7d05740 100644 --- a/gcc/ada/gnat_rm.texi +++ b/gcc/ada/gnat_rm.texi @@ -8501,7 +8501,9 @@ In addition, Ada allows implementations to define additional attributes whose meaning is defined by the implementation. GNAT provides a number of these implementation-dependent attributes which can be used to extend and enhance the functionality of the compiler. This section of -the GNAT reference manual describes these additional attributes. +the GNAT reference manual describes these additional attributes. It also +describes additional implementation-dependent features of standard +language-defined attributes. Note that any program using these attributes may not be portable to other compilers (although GNAT implements this set of attributes on all @@ -8983,7 +8985,8 @@ input-output functions for fixed-point values. @unnumberedsec Attribute From_Any @findex From_Any @noindent -PLEASE ADD DOCUMENTATION HERE??? +This internal attribute is used for the generation of remote subprogram +stubs in the context of the Distributed Systems Annex. @node Attribute Has_Access_Values @unnumberedsec Attribute Has_Access_Values @@ -9322,7 +9325,13 @@ statically matching subtypes. @unnumberedsec Attribute Old @findex Old @noindent -PLEASE ADD DOCUMENTATION HERE??? +In addition to the usage of Old defined in the Ada 2012 RM (usage +within @code{Post} aspect), GNAT also permits the use of this attribute +in implementation defined pragmas @code{Postcondition}, +@code{Loop_Entry}, and @code{Contract_Cases}. Also usages of +@code{Old} which would be illegal according to the Ada 2012 RM +definition are allowed under control of +implementation defined pragma @code{Allow_Unevaluated_Use_Of_Old}. @node Attribute Passed_By_Reference @unnumberedsec Attribute Passed_By_Reference @@ -9725,7 +9734,8 @@ a 32 bits machine). @unnumberedsec Attribute To_Any @findex To_Any @noindent -PLEASE ADD DOCUMENTATION HERE??? +This internal attribute is used for the generation of remote subprogram +stubs in the context of the Distributed Systems Annex. @node Attribute Type_Class @unnumberedsec Attribute Type_Class @@ -9759,13 +9769,17 @@ be compatible with the DEC Ada 83 attribute of the same name. @unnumberedsec Attribute Type_Key @findex Type_Key @noindent -PLEASE ADD DOCUMENTATION HERE??? +The @code{Type_Key} attribute is applicable to a type or subtype and +yields a value of type Standard.String containing encoded information +about the type or subtype. This provides improved compatibility with +other implementations that support this attribute. @node Attribute TypeCode @unnumberedsec Attribute TypeCode @findex TypeCode @noindent -PLEASE ADD DOCUMENTATION HERE??? +This internal attribute is used for the generation of remote subprogram +stubs in the context of the Distributed Systems Annex. @node Attribute UET_Address @unnumberedsec Attribute UET_Address diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index 479eb6ec39b..dc1d1c5090a 100644 --- a/gcc/ada/sinfo.ads +++ b/gcc/ada/sinfo.ads @@ -562,12 +562,20 @@ package Sinfo is -- not make sense from a user point-of-view, and that cross-references that -- do not lead to data dependences for subprograms can be safely ignored. - -- In addition pragma Debug statements are removed from the tree (rewritten - -- to NULL stmt), since they should be ignored in formal verification. + -- GNATprove relies on the following frontend behaviors: - -- An error is also issued for missing subunits, similar to the warning - -- issued when generating code, to avoid formal verification of a partial - -- unit. + -- 1. The first declarations in the list of visible declarations of + -- a package declaration for a generic instance, up to the first + -- declaration which comes from source, should correspond to + -- the "mappings nodes" between formal and actual generic parameters. + + -- 2. In addition pragma Debug statements are removed from the tree + -- (rewritten to NULL stmt), since they should be ignored in formal + -- verification. + + -- 3. An error is also issued for missing subunits, similar to the + -- warning issued when generating code, to avoid formal verification + -- of a partial unit. ----------------------- -- Check Flag Fields --