[multiple changes]
2013-10-17 Vincent Celier <celier@adacore.com> * gnat_ugn.texi: Remove VMS conversion of -gnatet and -gnateT, now that they are both in ug_words. * ug_words: Update qualifier for -gnatet Add qualifier for -gnateT * vms_data.ads: Update qualifier for -gnatet Add qualifier for -gnateT * projects.texi: Continue to update the project documentation for VMS. 2013-10-17 Robert Dewar <dewar@adacore.com> * einfo.ads, einfo.adb (Has_Body_References): New flag. (Body_References): New field. * sem_prag.adb (Record_Possible_Body_Reference): New procedure (Analyze_Input_Output): Call Record_Possible_Body_Reference (Analyze_Global_Item): Call Record_Possible_Body_Reference (Analyze_Refinement_Clause): Output messages if illegal global refs. 2013-10-17 Thomas Quinot <quinot@adacore.com> * freeze.adb (Check_Component_Storage_Order): Reject a record or array type that does not have an explicit Scalar_Storage_Order attribute definition if a component of the record, or the elements of the array, have one. * gnat_rm.texi (attribute Scalar_Storage_Order): Document the above rule. From-SVN: r203750
This commit is contained in:
parent
455f333611
commit
8a7c040046
@ -1,3 +1,31 @@
|
||||
2013-10-17 Vincent Celier <celier@adacore.com>
|
||||
|
||||
* gnat_ugn.texi: Remove VMS conversion of -gnatet and -gnateT,
|
||||
now that they are both in ug_words.
|
||||
* ug_words: Update qualifier for -gnatet Add qualifier for -gnateT
|
||||
* vms_data.ads: Update qualifier for -gnatet Add qualifier
|
||||
for -gnateT
|
||||
* projects.texi: Continue to update the project documentation
|
||||
for VMS.
|
||||
|
||||
2013-10-17 Robert Dewar <dewar@adacore.com>
|
||||
|
||||
* einfo.ads, einfo.adb (Has_Body_References): New flag.
|
||||
(Body_References): New field.
|
||||
* sem_prag.adb (Record_Possible_Body_Reference): New procedure
|
||||
(Analyze_Input_Output): Call Record_Possible_Body_Reference
|
||||
(Analyze_Global_Item): Call Record_Possible_Body_Reference
|
||||
(Analyze_Refinement_Clause): Output messages if illegal global refs.
|
||||
|
||||
2013-10-17 Thomas Quinot <quinot@adacore.com>
|
||||
|
||||
* freeze.adb (Check_Component_Storage_Order): Reject a record or
|
||||
array type that does not have an explicit Scalar_Storage_Order
|
||||
attribute definition if a component of the record, or the
|
||||
elements of the array, have one.
|
||||
* gnat_rm.texi (attribute Scalar_Storage_Order): Document the above
|
||||
rule.
|
||||
|
||||
2013-10-17 Vincent Celier <celier@adacore.com>
|
||||
|
||||
* gnat_ugn.texi: Add examples of switches -gnateD, including
|
||||
|
@ -132,6 +132,7 @@ package body Einfo is
|
||||
-- String_Literal_Low_Bound Node15
|
||||
|
||||
-- Access_Disp_Table Elist16
|
||||
-- Body_References Elist16
|
||||
-- Cloned_Subtype Node16
|
||||
-- DTC_Entity Node16
|
||||
-- Entry_Formal Node16
|
||||
@ -552,8 +553,8 @@ package body Einfo is
|
||||
-- Has_Delayed_Rep_Aspects Flag261
|
||||
-- May_Inherit_Delayed_Rep_Aspects Flag262
|
||||
-- Has_Visible_Refinement Flag263
|
||||
-- Has_Body_References Flag264
|
||||
|
||||
-- (unused) Flag264
|
||||
-- (unused) Flag265
|
||||
-- (unused) Flag266
|
||||
-- (unused) Flag267
|
||||
@ -733,6 +734,12 @@ package body Einfo is
|
||||
return Flag40 (Id);
|
||||
end Body_Needed_For_SAL;
|
||||
|
||||
function Body_References (Id : E) return L is
|
||||
begin
|
||||
pragma Assert (Ekind (Id) = E_Abstract_State);
|
||||
return Elist16 (Id);
|
||||
end Body_References;
|
||||
|
||||
function C_Pass_By_Copy (Id : E) return B is
|
||||
begin
|
||||
pragma Assert (Is_Record_Type (Id));
|
||||
@ -1294,6 +1301,12 @@ package body Einfo is
|
||||
return Flag139 (Id);
|
||||
end Has_Biased_Representation;
|
||||
|
||||
function Has_Body_References (Id : E) return B is
|
||||
begin
|
||||
pragma Assert (Ekind (Id) = E_Abstract_State);
|
||||
return Flag264 (Id);
|
||||
end Has_Body_References;
|
||||
|
||||
function Has_Completion (Id : E) return B is
|
||||
begin
|
||||
return Flag26 (Id);
|
||||
@ -3336,6 +3349,12 @@ package body Einfo is
|
||||
Set_Flag40 (Id, V);
|
||||
end Set_Body_Needed_For_SAL;
|
||||
|
||||
procedure Set_Body_References (Id : E; V : L) is
|
||||
begin
|
||||
pragma Assert (Ekind (Id) = E_Abstract_State);
|
||||
Set_Elist16 (Id, V);
|
||||
end Set_Body_References;
|
||||
|
||||
procedure Set_C_Pass_By_Copy (Id : E; V : B := True) is
|
||||
begin
|
||||
pragma Assert (Is_Record_Type (Id) and then Is_Base_Type (Id));
|
||||
@ -3909,6 +3928,12 @@ package body Einfo is
|
||||
Set_Flag139 (Id, V);
|
||||
end Set_Has_Biased_Representation;
|
||||
|
||||
procedure Set_Has_Body_References (Id : E; V : B := True) is
|
||||
begin
|
||||
pragma Assert (Ekind (Id) = E_Abstract_State);
|
||||
Set_Flag264 (Id, V);
|
||||
end Set_Has_Body_References;
|
||||
|
||||
procedure Set_Has_Completion (Id : E; V : B := True) is
|
||||
begin
|
||||
Set_Flag26 (Id, V);
|
||||
@ -7984,6 +8009,7 @@ package body Einfo is
|
||||
W ("Has_Anonymous_Master", Flag253 (Id));
|
||||
W ("Has_Atomic_Components", Flag86 (Id));
|
||||
W ("Has_Biased_Representation", Flag139 (Id));
|
||||
W ("Has_Body_References", Flag264 (Id));
|
||||
W ("Has_Completion", Flag26 (Id));
|
||||
W ("Has_Completion_In_Body", Flag71 (Id));
|
||||
W ("Has_Complex_Representation", Flag140 (Id));
|
||||
@ -8672,6 +8698,10 @@ package body Einfo is
|
||||
procedure Write_Field16_Name (Id : Entity_Id) is
|
||||
begin
|
||||
case Ekind (Id) is
|
||||
|
||||
when E_Abstract_State =>
|
||||
Write_Str ("Body_References");
|
||||
|
||||
when E_Record_Type |
|
||||
E_Record_Type_With_Private =>
|
||||
Write_Str ("Access_Disp_Table");
|
||||
|
@ -493,6 +493,12 @@ package Einfo is
|
||||
-- units. Indicates that the source for the body must be included
|
||||
-- when the unit is part of a standalone library.
|
||||
|
||||
-- Body_References (Elist16)
|
||||
-- Defined in abstract state entities. Only set if Has_Body_References
|
||||
-- flag is set True, in which case it contains an element list of global
|
||||
-- references (identifiers) in the current package body to this abstract
|
||||
-- state that are illegal if the abstract state has a visible refinement.
|
||||
|
||||
-- C_Pass_By_Copy (Flag125) [implementation base type only]
|
||||
-- Defined in record types. Set if a pragma Convention for the record
|
||||
-- type specifies convention C_Pass_By_Copy. This convention name is
|
||||
@ -1405,6 +1411,10 @@ package Einfo is
|
||||
-- size of the type, forcing biased representation for the object, but
|
||||
-- the subtype is still an unbiased type.
|
||||
|
||||
-- Has_Body_References (Flag264)
|
||||
-- Defined in entities for abstract states. Set if Body_References has
|
||||
-- at least one entry.
|
||||
|
||||
-- Has_Completion (Flag26)
|
||||
-- Defined in all entities that require a completion (functions,
|
||||
-- procedures, private types, limited private types, incomplete types,
|
||||
@ -5117,6 +5127,8 @@ package Einfo is
|
||||
-- E_Abstract_State
|
||||
-- Refinement_Constituents (Elist8)
|
||||
-- Refined_State (Node10)
|
||||
-- Body_References (Elist16)
|
||||
-- Has_Body_References (Flag264)
|
||||
-- Has_Visible_Refinement (Flag263)
|
||||
-- Has_Non_Null_Refinement (synth)
|
||||
-- Has_Null_Refinement (synth)
|
||||
@ -6230,6 +6242,7 @@ package Einfo is
|
||||
function Block_Node (Id : E) return N;
|
||||
function Body_Entity (Id : E) return E;
|
||||
function Body_Needed_For_SAL (Id : E) return B;
|
||||
function Body_References (Id : E) return L;
|
||||
function CR_Discriminant (Id : E) return E;
|
||||
function C_Pass_By_Copy (Id : E) return B;
|
||||
function Can_Never_Be_Null (Id : E) return B;
|
||||
@ -6325,6 +6338,7 @@ package Einfo is
|
||||
function Has_Anonymous_Master (Id : E) return B;
|
||||
function Has_Atomic_Components (Id : E) return B;
|
||||
function Has_Biased_Representation (Id : E) return B;
|
||||
function Has_Body_References (Id : E) return B;
|
||||
function Has_Completion (Id : E) return B;
|
||||
function Has_Completion_In_Body (Id : E) return B;
|
||||
function Has_Complex_Representation (Id : E) return B;
|
||||
@ -6848,6 +6862,7 @@ package Einfo is
|
||||
procedure Set_Block_Node (Id : E; V : N);
|
||||
procedure Set_Body_Entity (Id : E; V : E);
|
||||
procedure Set_Body_Needed_For_SAL (Id : E; V : B := True);
|
||||
procedure Set_Body_References (Id : E; V : L);
|
||||
procedure Set_CR_Discriminant (Id : E; V : E);
|
||||
procedure Set_C_Pass_By_Copy (Id : E; V : B := True);
|
||||
procedure Set_Can_Never_Be_Null (Id : E; V : B := True);
|
||||
@ -6942,6 +6957,7 @@ package Einfo is
|
||||
procedure Set_Has_Anonymous_Master (Id : E; V : B := True);
|
||||
procedure Set_Has_Atomic_Components (Id : E; V : B := True);
|
||||
procedure Set_Has_Biased_Representation (Id : E; V : B := True);
|
||||
procedure Set_Has_Body_References (Id : E; V : B := True);
|
||||
procedure Set_Has_Completion (Id : E; V : B := True);
|
||||
procedure Set_Has_Completion_In_Body (Id : E; V : B := True);
|
||||
procedure Set_Has_Complex_Representation (Id : E; V : B := True);
|
||||
@ -7568,6 +7584,7 @@ package Einfo is
|
||||
pragma Inline (Block_Node);
|
||||
pragma Inline (Body_Entity);
|
||||
pragma Inline (Body_Needed_For_SAL);
|
||||
pragma Inline (Body_References);
|
||||
pragma Inline (CR_Discriminant);
|
||||
pragma Inline (C_Pass_By_Copy);
|
||||
pragma Inline (Can_Never_Be_Null);
|
||||
@ -7660,6 +7677,7 @@ package Einfo is
|
||||
pragma Inline (Has_Anonymous_Master);
|
||||
pragma Inline (Has_Atomic_Components);
|
||||
pragma Inline (Has_Biased_Representation);
|
||||
pragma Inline (Has_Body_References);
|
||||
pragma Inline (Has_Completion);
|
||||
pragma Inline (Has_Completion_In_Body);
|
||||
pragma Inline (Has_Complex_Representation);
|
||||
@ -8031,6 +8049,7 @@ package Einfo is
|
||||
pragma Inline (Set_Block_Node);
|
||||
pragma Inline (Set_Body_Entity);
|
||||
pragma Inline (Set_Body_Needed_For_SAL);
|
||||
pragma Inline (Set_Body_References);
|
||||
pragma Inline (Set_CR_Discriminant);
|
||||
pragma Inline (Set_C_Pass_By_Copy);
|
||||
pragma Inline (Set_Can_Never_Be_Null);
|
||||
@ -8121,6 +8140,7 @@ package Einfo is
|
||||
pragma Inline (Set_Has_Anonymous_Master);
|
||||
pragma Inline (Set_Has_Atomic_Components);
|
||||
pragma Inline (Set_Has_Biased_Representation);
|
||||
pragma Inline (Set_Has_Body_References);
|
||||
pragma Inline (Set_Has_Completion);
|
||||
pragma Inline (Set_Has_Completion_In_Body);
|
||||
pragma Inline (Set_Has_Complex_Representation);
|
||||
|
@ -92,11 +92,15 @@ package body Freeze is
|
||||
|
||||
procedure Check_Component_Storage_Order
|
||||
(Encl_Type : Entity_Id;
|
||||
Comp : Entity_Id);
|
||||
Comp : Entity_Id;
|
||||
ADC : Node_Id);
|
||||
-- For an Encl_Type that has a Scalar_Storage_Order attribute definition
|
||||
-- clause, verify that the component type is compatible. For arrays,
|
||||
-- Comp is Empty; for records, it is the entity of the component under
|
||||
-- consideration.
|
||||
-- clause, verify that the component type has an explicit and compatible
|
||||
-- attribute/aspect. For arrays, Comp is Empty; for records, it is the
|
||||
-- entity of the component under consideration. For an Encl_Type that
|
||||
-- does not have a Scalar_Storage_Order attribute definition clause,
|
||||
-- verify that the component also does not have such a clause.
|
||||
-- ADC is the attribute definition clause if present (or Empty).
|
||||
|
||||
procedure Check_Strict_Alignment (E : Entity_Id);
|
||||
-- E is a base type. If E is tagged or has a component that is aliased
|
||||
@ -1068,11 +1072,12 @@ package body Freeze is
|
||||
|
||||
procedure Check_Component_Storage_Order
|
||||
(Encl_Type : Entity_Id;
|
||||
Comp : Entity_Id)
|
||||
Comp : Entity_Id;
|
||||
ADC : Node_Id)
|
||||
is
|
||||
Comp_Type : Entity_Id;
|
||||
Comp_ADC : Node_Id;
|
||||
Err_Node : Node_Id;
|
||||
ADC : Node_Id;
|
||||
|
||||
Comp_Byte_Aligned : Boolean;
|
||||
-- Set True for the record case, when Comp starts on a byte boundary
|
||||
@ -1113,11 +1118,24 @@ package body Freeze is
|
||||
-- the attribute definition clause is attached to the first subtype.
|
||||
|
||||
Comp_Type := Base_Type (Comp_Type);
|
||||
ADC := Get_Attribute_Definition_Clause
|
||||
(First_Subtype (Comp_Type),
|
||||
Attribute_Scalar_Storage_Order);
|
||||
Comp_ADC := Get_Attribute_Definition_Clause
|
||||
(First_Subtype (Comp_Type),
|
||||
Attribute_Scalar_Storage_Order);
|
||||
|
||||
if Is_Record_Type (Comp_Type) or else Is_Array_Type (Comp_Type) then
|
||||
-- Case of enclosing type not having explicit SSO: component cannot
|
||||
-- have it either.
|
||||
|
||||
if No (ADC) then
|
||||
if Present (Comp_ADC) then
|
||||
Error_Msg_N
|
||||
("composite type must have explicit scalar storage order",
|
||||
Err_Node);
|
||||
end if;
|
||||
|
||||
-- Case of enclosing type having explicit SSO: check compatible
|
||||
-- attribute on Comp_Type if composite.
|
||||
|
||||
elsif Is_Record_Type (Comp_Type) or else Is_Array_Type (Comp_Type) then
|
||||
if Present (Comp) and then Chars (Comp) = Name_uParent then
|
||||
if Reverse_Storage_Order (Encl_Type)
|
||||
/=
|
||||
@ -1142,6 +1160,9 @@ package body Freeze is
|
||||
& "storage order as enclosing composite", Err_Node);
|
||||
end if;
|
||||
|
||||
-- Enclosing type has explicit SSO, non-composite component must not
|
||||
-- be aliased.
|
||||
|
||||
elsif Component_Aliased then
|
||||
Error_Msg_N
|
||||
("aliased component not permitted for type with "
|
||||
@ -2312,11 +2333,12 @@ package body Freeze is
|
||||
|
||||
-- Check for scalar storage order
|
||||
|
||||
if Present (Get_Attribute_Definition_Clause
|
||||
(Arr, Attribute_Scalar_Storage_Order))
|
||||
then
|
||||
Check_Component_Storage_Order (Arr, Empty);
|
||||
end if;
|
||||
Check_Component_Storage_Order
|
||||
(Encl_Type => Arr,
|
||||
Comp => Empty,
|
||||
ADC => Get_Attribute_Definition_Clause
|
||||
(First_Subtype (Arr),
|
||||
Attribute_Scalar_Storage_Order));
|
||||
|
||||
-- Processing that is done only for subtypes
|
||||
|
||||
@ -2999,16 +3021,17 @@ package body Freeze is
|
||||
("??scalar storage order specified but no component clause",
|
||||
ADC);
|
||||
end if;
|
||||
|
||||
-- Check attribute on component types
|
||||
|
||||
Comp := First_Component (Rec);
|
||||
while Present (Comp) loop
|
||||
Check_Component_Storage_Order (Rec, Comp);
|
||||
Next_Component (Comp);
|
||||
end loop;
|
||||
end if;
|
||||
|
||||
-- Check consistent attribute setting on component types
|
||||
|
||||
Comp := First_Component (Rec);
|
||||
while Present (Comp) loop
|
||||
Check_Component_Storage_Order
|
||||
(Encl_Type => Rec, Comp => Comp, ADC => ADC);
|
||||
Next_Component (Comp);
|
||||
end loop;
|
||||
|
||||
-- Deal with Bit_Order aspect specifying a non-default bit order
|
||||
|
||||
ADC := Get_Attribute_Definition_Clause (Rec, Attribute_Bit_Order);
|
||||
|
@ -8727,6 +8727,10 @@ have a @code{Scalar_Storage_Order} attribute definition clause. In addition,
|
||||
if the component does not start on a byte boundary, then the scalar storage
|
||||
order specified for S and for the nested component type shall be identical.
|
||||
|
||||
If @var{S} appears as the type of a record or array component, the enclosing
|
||||
record or array shall also have a @code{Scalar_Storage_Order} attribute
|
||||
definition clause.
|
||||
|
||||
No component of a type that has a @code{Scalar_Storage_Order} attribute
|
||||
definition may be aliased.
|
||||
|
||||
|
@ -3825,12 +3825,12 @@ temporary use of special test software.
|
||||
@cindex @option{-gnateS} (@command{gcc})
|
||||
Synonym of @option{-fdump-scos}, kept for backards compatibility.
|
||||
|
||||
@item ^-gnatet^/TARGET_DEPENDENT_INFO^=@var{path}
|
||||
@item -gnatet=@var{path}
|
||||
@cindex @option{-gnatet=file} (@command{gcc})
|
||||
Generate target dependent information. The format of the output file is
|
||||
described in the section about switch @option{-gnateT}.
|
||||
|
||||
@item ^-gnateT^/TARGET_DEPENDENT_INFO^=@var{path}
|
||||
@item -gnateT=@var{path}
|
||||
@cindex @option{-gnateT} (@command{gcc})
|
||||
Read target dependent information, such as endianness or sizes and alignments
|
||||
of base type. If this switch is passed, the default target dependent
|
||||
|
@ -3170,10 +3170,10 @@ The following packages are currently supported in project files
|
||||
@command{gnatfind} via the @command{gnat} driver. Its attributes
|
||||
@b{Default_Switches} and @b{^Switches^Switches^} have the same semantics as for the
|
||||
package @code{Builder}.
|
||||
@item Gnatls
|
||||
@item ^Gnatls^Gnatls^
|
||||
This package the options to use when invoking @command{gnatls} via the
|
||||
@command{gnat} driver.
|
||||
@item Gnatstub
|
||||
@item ^Gnatstub^Gnatstub^
|
||||
This package specifies the options used when calling the tool
|
||||
@command{gnatstub} via the @command{gnat} driver. Its attributes
|
||||
@b{Default_Switches} and @b{^Switches^Switches^} have the same semantics as for the
|
||||
@ -3630,8 +3630,8 @@ end MyProj;
|
||||
* Package Cross_Reference Attributes::
|
||||
* Package Eliminate Attributes::
|
||||
* Package Finder Attributes::
|
||||
* Package gnatls Attributes::
|
||||
* Package gnatstub Attributes::
|
||||
* Package ^gnatls^gnatls^ Attributes::
|
||||
* Package ^gnatstub^gnatstub^ Attributes::
|
||||
* Package IDE Attributes::
|
||||
* Package Install Attributes::
|
||||
* Package Linker Attributes::
|
||||
@ -4630,8 +4630,8 @@ invoking @code{gnatfind} for the source.
|
||||
|
||||
@end itemize
|
||||
|
||||
@node Package gnatls Attributes
|
||||
@subsubsection Package gnatls Attributes
|
||||
@node Package ^gnatls^gnatls^ Attributes
|
||||
@subsubsection Package ^gnatls^gnatls^ Attributes
|
||||
|
||||
@itemize @bullet
|
||||
|
||||
@ -4641,8 +4641,8 @@ Value is a list of switches to be used when invoking @code{gnatls}.
|
||||
|
||||
@end itemize
|
||||
|
||||
@node Package gnatstub Attributes
|
||||
@subsubsection Package gnatstub Attributes
|
||||
@node Package ^gnatstub^gnatstub^ Attributes
|
||||
@subsubsection Package ^gnatstub^gnatstub^ Attributes
|
||||
|
||||
@itemize @bullet
|
||||
|
||||
@ -4650,7 +4650,7 @@ Value is a list of switches to be used when invoking @code{gnatls}.
|
||||
|
||||
Index is a language name. Value is a list of switches to be used when invoking
|
||||
@code{gnatstub} for a source of the language, if there is no applicable
|
||||
attribute Switches.
|
||||
attribute ^Switches^Switches^.
|
||||
|
||||
@item @b{^Switches^Switches^}: list, optional index, indexed, case-insensitive index,
|
||||
others allowed
|
||||
@ -4699,11 +4699,11 @@ the handling of switches.
|
||||
Value is a string that specifies the name of the debugger to be used, such as
|
||||
gdb, powerpc-wrs-vxworks-gdb or gdb-4.
|
||||
|
||||
@item @b{gnatlist}: single
|
||||
@item @b{^gnatlist^gnatlist^}: single
|
||||
|
||||
Value is a string that specifies the name of the @command{gnatls} utility
|
||||
Value is a string that specifies the name of the @command{^gnatls^gnatls^} utility
|
||||
to be used to retrieve information about the predefined path; for example,
|
||||
@code{"gnatls"}, @code{"powerpc-wrs-vxworks-gnatls"}.
|
||||
@code{"^gnatls^gnatls^"}, @code{"powerpc-wrs-vxworks-gnatls"}.
|
||||
|
||||
@item @b{VCS_Kind}: single
|
||||
|
||||
|
@ -277,23 +277,30 @@ package body Sem_Prag is
|
||||
-- of a Test_Case pragma if present (possibly Empty). We treat these as
|
||||
-- spec expressions (i.e. similar to a default expression).
|
||||
|
||||
procedure Record_Possible_Body_Reference
|
||||
(Item : Node_Id;
|
||||
Item_Id : Entity_Id);
|
||||
-- Given an entity reference (Item) and the corresponding Entity (Item_Id),
|
||||
-- determines if we have a body reference to an abstract state, which may
|
||||
-- be illegal if the state is refined within the body.
|
||||
|
||||
procedure Rewrite_Assertion_Kind (N : Node_Id);
|
||||
-- If N is Pre'Class, Post'Class, Invariant'Class, or Type_Invariant'Class,
|
||||
-- then it is rewritten as an identifier with the corresponding special
|
||||
-- name _Pre, _Post, _Invariant, or _Type_Invariant. Used by pragmas
|
||||
-- Check, Check_Policy.
|
||||
|
||||
procedure Set_Unit_Name (N : Node_Id; With_Item : Node_Id);
|
||||
-- Place semantic information on the argument of an Elaborate/Elaborate_All
|
||||
-- pragma. Entity name for unit and its parents is taken from item in
|
||||
-- previous with_clause that mentions the unit.
|
||||
|
||||
procedure rv;
|
||||
-- This is a dummy function called by the processing for pragma Reviewable.
|
||||
-- It is there for assisting front end debugging. By placing a Reviewable
|
||||
-- pragma in the source program, a breakpoint on rv catches this place in
|
||||
-- the source, allowing convenient stepping to the point of interest.
|
||||
|
||||
procedure Set_Unit_Name (N : Node_Id; With_Item : Node_Id);
|
||||
-- Place semantic information on the argument of an Elaborate/Elaborate_All
|
||||
-- pragma. Entity name for unit and its parents is taken from item in
|
||||
-- previous with_clause that mentions the unit.
|
||||
|
||||
--------------
|
||||
-- Add_Item --
|
||||
--------------
|
||||
@ -772,6 +779,8 @@ package body Sem_Prag is
|
||||
|
||||
Item_Id := Entity_Of (Item);
|
||||
|
||||
Record_Possible_Body_Reference (Item, Item_Id);
|
||||
|
||||
if Present (Item_Id) then
|
||||
if Ekind_In (Item_Id, E_Abstract_State,
|
||||
E_In_Parameter,
|
||||
@ -1645,6 +1654,7 @@ package body Sem_Prag is
|
||||
Item_Id := Entity_Of (Item);
|
||||
|
||||
if Present (Item_Id) then
|
||||
Record_Possible_Body_Reference (Item, Item_Id);
|
||||
|
||||
-- A global item may denote a formal parameter of an enclosing
|
||||
-- subprogram. Do this check first to provide a better error
|
||||
@ -21641,6 +21651,29 @@ package body Sem_Prag is
|
||||
("& must denote an abstract state", State, State_Id);
|
||||
end if;
|
||||
|
||||
-- Enforce SPARK RM (6.1.5(4)): A global item shall not
|
||||
-- denote a state abstraction whose refinement is visible
|
||||
-- (a state abstraction cannot be named within its enclosing
|
||||
-- package's body other than in its refinement).
|
||||
|
||||
if Has_Body_References (State_Id) then
|
||||
declare
|
||||
Ref : Elmt_Id;
|
||||
Nod : Node_Id;
|
||||
begin
|
||||
Ref := First_Elmt (Body_References (State_Id));
|
||||
while Present (Ref) loop
|
||||
Nod := Node (Ref);
|
||||
Error_Msg_N
|
||||
("global reference to & not allowed "
|
||||
& "(SPARK RM 6.1.5(4))", Nod);
|
||||
Error_Msg_Sloc := Sloc (State);
|
||||
Error_Msg_N ("\refinement of & is visible#", Nod);
|
||||
Next_Elmt (Ref);
|
||||
end loop;
|
||||
end;
|
||||
end if;
|
||||
|
||||
-- The state name is illegal
|
||||
|
||||
else
|
||||
@ -23296,6 +23329,27 @@ package body Sem_Prag is
|
||||
|
||||
end Process_Compilation_Unit_Pragmas;
|
||||
|
||||
------------------------------------
|
||||
-- Record_Possible_Body_Reference --
|
||||
------------------------------------
|
||||
|
||||
procedure Record_Possible_Body_Reference
|
||||
(Item : Node_Id;
|
||||
Item_Id : Entity_Id)
|
||||
is
|
||||
begin
|
||||
if In_Package_Body
|
||||
and then Ekind (Item_Id) = E_Abstract_State
|
||||
then
|
||||
if not Has_Body_References (Item_Id) then
|
||||
Set_Has_Body_References (Item_Id, True);
|
||||
Set_Body_References (Item_Id, New_Elmt_List);
|
||||
end if;
|
||||
|
||||
Append_Elmt (Item, Body_References (Item_Id));
|
||||
end if;
|
||||
end Record_Possible_Body_Reference;
|
||||
|
||||
------------------------------
|
||||
-- Relocate_Pragmas_To_Body --
|
||||
------------------------------
|
||||
|
@ -72,7 +72,8 @@ gcc -c ^ GNAT COMPILE
|
||||
-gnatep ^ /DATA_PREPROCESSING
|
||||
-gnateP ^ /CATEGORIZATION_WARNINGS
|
||||
-gnateS ^ /SCO_OUTPUT
|
||||
-gnatet ^ /TARGET_DEPENDENT_INFO
|
||||
-gnatet ^ /WRITE_TARGET_DEPENDENT_INFO
|
||||
-gnateT ^ /READ_TARGET_DEPENDENT_INFO
|
||||
-gnateV ^ /PARAMETER_VALIDITY_CHECK
|
||||
-gnateY ^ /IGNORE_STYLE_CHECKS_PRAGMAS
|
||||
-gnatE ^ /CHECKS=ELABORATION
|
||||
|
@ -2885,12 +2885,17 @@ package VMS_Data is
|
||||
--
|
||||
-- All compiler tables start at nnn times usual starting size.
|
||||
|
||||
S_GCC_Target : aliased constant S := "/TARGET_DEPENDENT_INFO " &
|
||||
"-gnatet";
|
||||
-- /NOTARGET_DEPENDENT_INFO (D)
|
||||
-- /TARGET_DEPENDENT_INFO
|
||||
S_GCC_Target_W : aliased constant S := "/WRITE_TARGET_DEPENDENT_INFO=<" &
|
||||
"-gnatet=>";
|
||||
-- /WRITE_TARGET_DEPENDENT_INFO=file
|
||||
--
|
||||
-- Generate target dependent information.
|
||||
-- Generate target dependent information to file.
|
||||
|
||||
S_GCC_Target_R : aliased constant S := "/READ_TARGET_DEPENDENT_INFO=<" &
|
||||
"-gnateT=>";
|
||||
-- /READ_TARGET_DEPENDENT_INFO=file
|
||||
--
|
||||
-- Read target dependent information from file.
|
||||
|
||||
S_GCC_Trace : aliased constant S := "/TRACE_UNITS " &
|
||||
"-gnatdc";
|
||||
@ -3743,7 +3748,8 @@ package VMS_Data is
|
||||
S_GCC_Symbol 'Access,
|
||||
S_GCC_Syntax 'Access,
|
||||
S_GCC_Table 'Access,
|
||||
S_GCC_Target 'Access,
|
||||
S_GCC_Target_W'Access,
|
||||
S_GCC_Target_R'Access,
|
||||
S_GCC_Trace 'Access,
|
||||
S_GCC_Tree 'Access,
|
||||
S_GCC_Trys 'Access,
|
||||
|
Loading…
Reference in New Issue
Block a user