+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.
* Pragma Check_Float_Overflow::
* Pragma Check_Name::
* Pragma Check_Policy::
+* Pragma CIL_Constructor::
* Pragma Comment::
* Pragma Common_Object::
* Pragma Compile_Time_Error::
* Pragma Interrupt_Handler::
* Pragma Interrupt_State::
* Pragma Invariant::
+* Pragma Java_Constructor::
+* Pragma Java_Interface::
* Pragma Keep_Names::
* Pragma License::
* Pragma Link_With::
* Pragma Check_Float_Overflow::
* Pragma Check_Name::
* Pragma Check_Policy::
+* Pragma CIL_Constructor::
* Pragma Comment::
* Pragma Common_Object::
* Pragma Compile_Time_Error::
* Pragma Interrupt_Handler::
* Pragma Interrupt_State::
* Pragma Invariant::
+* Pragma Java_Constructor::
+* Pragma Java_Interface::
* Pragma Keep_Names::
* Pragma License::
* Pragma Link_With::
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
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
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.
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
Version => Ada_Version));
return True;
+ -- Here if not inlined, or we ignore the inlining
+
else
return False;
end if;
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);
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;
----------------
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;
---------------------
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;
-----------
-- 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)))
projects / platform / upstream / gcc.git / commitdiff