2013-07-05 Robert Dewar <dewar@adacore.com>

	* gnat_rm.texi: Update doc on missing pragmas.
	* sem_ch12.adb: Minor comment additions.

2013-07-05  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Analyze_Pragma): Ensure that
	Contract_Cases, Depends and Global are analyzed when they apply
	to a subprogram compilation unit. The pragmas are all added
	unconditionally to the construct's contract. This ensures that
	proof tools can locate the pragmas.

2013-07-05  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch8.adb (Freeze_Actual_Profile): An instance within
	a generic unit does not freeze a generic private type of the
	enclosing generic. This rule must also apply to a type derived
	from a generic private type.



git-svn-id: https://gcc.gnu.org/svn/gcc/trunk@200704 138bc75d-0d04-0410-961f-82ee72b054a4

5 files changed, 143 insertions, 17 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 46c2dbebaa5..c395a27ca51 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,23 @@
+2013-07-05  Robert Dewar  <dewar@adacore.com>
+
+	* gnat_rm.texi: Update doc on missing pragmas.
+	* sem_ch12.adb: Minor comment additions.
+
+2013-07-05  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_prag.adb (Analyze_Pragma): Ensure that
+	Contract_Cases, Depends and Global are analyzed when they apply
+	to a subprogram compilation unit. The pragmas are all added
+	unconditionally to the construct's contract. This ensures that
+	proof tools can locate the pragmas.
+
+2013-07-05  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch8.adb (Freeze_Actual_Profile): An instance within
+	a generic unit does not freeze a generic private type of the
+	enclosing generic. This rule must also apply to a type derived
+	from a generic private type.
+
 2013-07-05  Arnaud Charlet  <charlet@adacore.com>
 
 	* gnat_rm.texi: Add missing documentation for pragmas.
diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi
index fb7cfa60603..19430091d59 100644
--- a/gcc/ada/gnat_rm.texi
+++ b/gcc/ada/gnat_rm.texi
@@ -117,6 +117,7 @@ Implementation Defined Pragmas
 * Pragma Check_Float_Overflow::
 * Pragma Check_Name::
 * Pragma Check_Policy::
+* Pragma CIL_Constructor::
 * Pragma Comment::
 * Pragma Common_Object::
 * Pragma Compile_Time_Error::
@@ -174,6 +175,8 @@ Implementation Defined Pragmas
 * Pragma Interrupt_Handler::
 * Pragma Interrupt_State::
 * Pragma Invariant::
+* Pragma Java_Constructor::
+* Pragma Java_Interface::
 * Pragma Keep_Names::
 * Pragma License::
 * Pragma Link_With::
@@ -926,6 +929,7 @@ consideration, the use of these pragmas should be minimized.
 * Pragma Check_Float_Overflow::
 * Pragma Check_Name::
 * Pragma Check_Policy::
+* Pragma CIL_Constructor::
 * Pragma Comment::
 * Pragma Common_Object::
 * Pragma Compile_Time_Error::
@@ -983,6 +987,8 @@ consideration, the use of these pragmas should be minimized.
 * Pragma Interrupt_Handler::
 * Pragma Interrupt_State::
 * Pragma Invariant::
+* Pragma Java_Constructor::
+* Pragma Java_Interface::
 * Pragma Keep_Names::
 * Pragma License::
 * Pragma Link_With::
@@ -1773,6 +1779,24 @@ compatibility with the standard @code{Assertion_Policy} pragma. The check
 policy setting @code{DISABLE} causes the second argument of a corresponding
 @code{Check} pragma to be completely ignored and not analyzed.
 
+@node Pragma CIL_Constructor
+@unnumberedsec Pragma CIL_Constructor
+@findex CIL_Constructor
+@noindent
+Syntax:
+
+@smallexample @c ada
+pragma CIL_Constructor ([Entity =>] function_LOCAL_NAME);
+@end smallexample
+
+@noindent
+This pragma is used to assert that the specified Ada function should be
+mapped to the .NET constructor for some Ada tagged record type.
+
+See section 4.1 of the
+@code{GNAT User's Guide: Supplement for the .NET Platform.}
+for related information.
+
 @node Pragma Comment
 @unnumberedsec Pragma Comment
 @findex Comment
@@ -3814,6 +3838,42 @@ 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.
 
+@node Pragma Java_Constructor
+@unnumberedsec Pragma Java_Constructor
+@findex Java_Constructor
+@noindent
+Syntax:
+
+@smallexample @c ada
+pragma Java_Constructor ([Entity =>] function_LOCAL_NAME);
+@end smallexample
+
+@noindent
+This pragma is used to assert that the specified Ada function should be
+mapped to the Java constructor for some Ada tagged record type.
+
+See section 7.3.2 of the
+@code{GNAT User's Guide: Supplement for the JVM Platform.}
+for related information.
+
+@node Pragma Java_Interface
+@unnumberedsec Pragma Java_Interface
+@findex Java_Interface
+@noindent
+Syntax:
+
+@smallexample @c ada
+pragma Java_Interface ([Entity =>] abstract_tagged_type_LOCAL_NAME);
+@end smallexample
+
+@noindent
+This pragma is used to assert that the specified Ada abstract tagged type
+is to be mapped to a Java interface name.
+
+See sections 7.1 and 7.2 of the
+@code{GNAT User's Guide: Supplement for the JVM Platform.}
+for related information.
+
 @node Pragma Keep_Names
 @unnumberedsec Pragma Keep_Names
 @findex Keep_Names
@@ -4388,7 +4448,7 @@ pragma No_Run_Time;
 This is an obsolete configuration pragma that historically was used to
 setup what is now called the "zero footprint" library. It causes any
 library units outside this basic library to be ignored. The use of
-this pragma has been superceded by the general configurable run-time
+this pragma has been superseded by the general configurable run-time
 capability of @code{GNAT} where the compiler takes into account whatever
 units happen to be accessible in the library.
 
diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb
index ed381b3ce5c..73b49658ea1 100644
--- a/gcc/ada/sem_ch12.adb
+++ b/gcc/ada/sem_ch12.adb
@@ -4367,19 +4367,30 @@ package body Sem_Ch12 is
       Subp : Entity_Id) return Boolean
    is
    begin
-      --  This complex conditional requires blow by blow comments ???
+      --  Must be inlined (or inlined renaming)
 
       if (Is_In_Main_Unit (N)
            or else Is_Inlined (Subp)
            or else Is_Inlined (Alias (Subp)))
+
+        --  Must be generating code or analyzing code in ASIS mode
+
         and then (Operating_Mode = Generate_Code
                    or else (Operating_Mode = Check_Semantics
                              and then ASIS_Mode))
+
         --  The body is needed when generating code (full expansion), in ASIS
         --  mode for other tools, and in SPARK mode (special expansion) for
         --  formal verification of the body itself.
+
         and then (Expander_Active or ASIS_Mode)
+
+        --  No point in inlining if ABE is inevitable
+
         and then not ABE_Is_Certain (N)
+
+        --  Or if subprogram is eliminated
+
         and then not Is_Eliminated (Subp)
       then
          Pending_Instantiations.Append
@@ -4392,6 +4403,8 @@ package body Sem_Ch12 is
              Version                  => Ada_Version));
          return True;
 
+      --  Here if not inlined, or we ignore the inlining
+
       else
          return False;
       end if;
diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb
index 1fbcf685a3d..f00300222d2 100644
--- a/gcc/ada/sem_ch8.adb
+++ b/gcc/ada/sem_ch8.adb
@@ -2069,11 +2069,20 @@ package body Sem_Ch8 is
 
                   if Is_Incomplete_Or_Private_Type (Etype (F))
                     and then No (Underlying_Type (Etype (F)))
-                    and then not Is_Generic_Type (Etype (F))
                   then
-                     Error_Msg_NE
-                       ("type& must be frozen before this point",
-                          Instantiation_Node, Etype (F));
+
+                     --  Exclude generic types, or types derived  from them.
+                     --  They will be frozen in the enclosing instance.
+
+                     if Is_Generic_Type (Etype (F))
+                       or else Is_Generic_Type (Root_Type (Etype (F)))
+                     then
+                        null;
+                     else
+                        Error_Msg_NE
+                          ("type& must be frozen before this point",
+                             Instantiation_Node, Etype (F));
+                     end if;
                   end if;
 
                   F := Next_Formal (F);
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 3f70c8f0552..08d6f9a30d5 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -10082,11 +10082,19 @@ package body Sem_Prag is
             if Nkind (Subp_Decl) = N_Subprogram_Body then
                Analyze_Contract_Cases_In_Decl_Part (N);
 
-            --  Chain the pragma on the contract for further processing
+            --  When Contract_Cases applies to a subprogram compilation unit,
+            --  the corresponding pragma is placed after the unit's declaration
+            --  node and needs to be analyzed immediately.
 
-            else
-               Add_Contract_Item (N, Subp_Id);
+            elsif Nkind (Subp_Decl) = N_Subprogram_Declaration
+              and then Nkind (Parent (Subp_Decl)) = N_Compilation_Unit
+            then
+               Analyze_Contract_Cases_In_Decl_Part (N);
             end if;
+
+            --  Chain the pragma on the contract for further processing
+
+            Add_Contract_Item (N, Subp_Id);
          end Contract_Cases;
 
          ----------------
@@ -10590,11 +10598,19 @@ package body Sem_Prag is
             if Nkind (Subp_Decl) = N_Subprogram_Body then
                Analyze_Depends_In_Decl_Part (N);
 
-            --  Chain the pragma on the contract for further processing
+            --  When Depends applies to a subprogram compilation unit, the
+            --  corresponding pragma is placed after the unit's declaration
+            --  node and needs to be analyzed immediately.
 
-            else
-               Add_Contract_Item (N, Subp_Id);
+            elsif Nkind (Subp_Decl) = N_Subprogram_Declaration
+              and then Nkind (Parent (Subp_Decl)) = N_Compilation_Unit
+            then
+               Analyze_Depends_In_Decl_Part (N);
             end if;
+
+            --  Chain the pragma on the contract for further processing
+
+            Add_Contract_Item (N, Subp_Id);
          end Depends;
 
          ---------------------
@@ -11833,11 +11849,19 @@ package body Sem_Prag is
             if Nkind (Subp_Decl) = N_Subprogram_Body then
                Analyze_Global_In_Decl_Part (N);
 
-            --  Chain the pragma on the contract for further processing
+            --  When Global applies to a subprogram compilation unit, the
+            --  corresponding pragma is placed after the unit's declaration
+            --  node and needs to be analyzed immediately.
 
-            else
-               Add_Contract_Item (N, Subp_Id);
+            elsif Nkind (Subp_Decl) = N_Subprogram_Declaration
+              and then Nkind (Parent (Subp_Decl)) = N_Compilation_Unit
+            then
+               Analyze_Global_In_Decl_Part (N);
             end if;
+
+            --  Chain the pragma on the contract for further processing
+
+            Add_Contract_Item (N, Subp_Id);
          end Global;
 
          -----------
@@ -13348,8 +13372,8 @@ package body Sem_Prag is
             --  abstract. ???
 
             if not Is_Tagged_Type (Typ) or else not Is_Abstract_Type (Typ) then
-               Error_Pragma_Arg ("pragma% requires an abstract "
-                 & "tagged type", Arg1);
+               Error_Pragma_Arg
+                 ("pragma% requires an abstract tagged type", Arg1);
 
             elsif not Has_Discriminants (Typ)
               or else Ekind (Etype (First_Discriminant (Typ)))