+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
-- String_Literal_Low_Bound Node15
-- Access_Disp_Table Elist16
+ -- Body_References Elist16
-- Cloned_Subtype Node16
-- DTC_Entity Node16
-- Entry_Formal Node16
-- 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
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));
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);
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));
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);
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));
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");
-- 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
-- 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,
-- 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)
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;
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;
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);
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);
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);
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);
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);
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);
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
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
-- 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)
/=
& "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 "
-- 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
("??scalar storage order specified but no component clause",
ADC);
end if;
+ end if;
- -- Check attribute on component types
+ -- Check consistent attribute setting on component types
- Comp := First_Component (Rec);
- while Present (Comp) loop
- Check_Component_Storage_Order (Rec, Comp);
- Next_Component (Comp);
- end loop;
- end if;
+ 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
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.
@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
@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
* 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::
@end itemize
-@node Package gnatls Attributes
-@subsubsection Package gnatls Attributes
+@node Package ^gnatls^gnatls^ Attributes
+@subsubsection Package ^gnatls^gnatls^ Attributes
@itemize @bullet
@end itemize
-@node Package gnatstub Attributes
-@subsubsection Package gnatstub Attributes
+@node Package ^gnatstub^gnatstub^ Attributes
+@subsubsection Package ^gnatstub^gnatstub^ Attributes
@itemize @bullet
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
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
-- 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 --
--------------
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,
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
("& 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
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 --
------------------------------
-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
--
-- 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";
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,
projects / thirdparty / gcc.git / commitdiff
