OpenE2K
/
gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[multiple changes] 

2016-04-18  Eric Botcazou  <ebotcazou@adacore.com>

	* layout.adb (Set_Elem_Alignment): Extend setting of alignment
	to subtypes that are not first subtypes.

2016-04-18  Ed Schonberg  <schonberg@adacore.com>

	* sem_prag.ads (Collect_Inherited_Class_Wide_Conditions):
	Simplify interface.
	* sem_prag.adb (Collect_Inherited_Class_Wide_Conditions): Insert
	generated pragmas after subprogram declaration, rather than in
	the corresponding subprogram body.
	* sem_ch6.adb (New_Overloaded_Entity): In GNATProve
	mode, if the operation is overridding, call
	Collect_Inherited_Class_Wide_Conditions to generate the
	corresponding pragmas immediately after the corresponding
	subprogram declaration.

2016-04-18  Arnaud Charlet  <charlet@adacore.com>

	* spark_xrefs.ads (Xref_Index, Scope_Index, File_Index): restrict
	type to natural numbers.
	(Stype): document code characters for concurrent entities.

2016-04-18  Olivier Hainque  <hainque@adacore.com>

	* targparm.ads: Update the Frontend_Exceptions default internal
	value.
	(Frontend_Exceptions_On_Target): Change default value to True.

2016-04-18  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch4.adb (Analyze_Selected_Component): Refine error
	detection when a selected component in the body of a synchronized
	type is a reference to an object of the same type declared
	elsewhere. The construct is legal if the prefix of the selected
	component includes an explicit dereference at any point.

From-SVN: r235118
This commit is contained in:
Arnaud Charlet 2016-04-18 12:30:27 +02:00
parent 070d862dde
commit 0f6251c7ac
8 changed files with 233 additions and 120 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

38
gcc/ada/ChangeLog
View File

@ -1,3 +1,41 @@
2016-04-18 Eric Botcazou <ebotcazou@adacore.com>
* layout.adb (Set_Elem_Alignment): Extend setting of alignment
to subtypes that are not first subtypes.
2016-04-18 Ed Schonberg <schonberg@adacore.com>
* sem_prag.ads (Collect_Inherited_Class_Wide_Conditions):
Simplify interface.
* sem_prag.adb (Collect_Inherited_Class_Wide_Conditions): Insert
generated pragmas after subprogram declaration, rather than in
the corresponding subprogram body.
* sem_ch6.adb (New_Overloaded_Entity): In GNATProve
mode, if the operation is overridding, call
Collect_Inherited_Class_Wide_Conditions to generate the
corresponding pragmas immediately after the corresponding
subprogram declaration.
2016-04-18 Arnaud Charlet <charlet@adacore.com>
* spark_xrefs.ads (Xref_Index, Scope_Index, File_Index): restrict
type to natural numbers.
(Stype): document code characters for concurrent entities.
2016-04-18 Olivier Hainque <hainque@adacore.com>
* targparm.ads: Update the Frontend_Exceptions default internal
value.
(Frontend_Exceptions_On_Target): Change default value to True.
2016-04-18 Ed Schonberg <schonberg@adacore.com>
* sem_ch4.adb (Analyze_Selected_Component): Refine error
detection when a selected component in the body of a synchronized
type is a reference to an object of the same type declared
elsewhere. The construct is legal if the prefix of the selected
component includes an explicit dereference at any point.
2016-04-18 Hristian Kirtchev <kirtchev@adacore.com>
* sem_ch3.adb (Analyze_Object_Declaration): Do not consider

180
gcc/ada/layout.adb
View File

@ -3268,80 +3268,114 @@ package body Layout is
elsif Alignment (E) = A then
null;
-- Now we come to the difficult cases where we have inherited an
-- alignment and size, but overridden the size but not the alignment.
elsif Has_Size_Clause (E) or else Has_Object_Size_Clause (E) then
-- This is tricky, it might be thought that we should try to
-- inherit the alignment, since that's what the RM implies, but
-- that leads to complex rules and oddities. Consider for example:
-- type R is new Character;
-- for R'Size use 16;
-- It seems quite bogus in this case to inherit an alignment of 1
-- from the parent type Character. Furthermore, if that's what the
-- programmer really wanted for some odd reason, then he could
-- specify the alignment directly.
-- Furthermore we really don't want to inherit the alignment in
-- the case of a specified Object_Size for a subtype, since then
-- there would be no way of overriding to give a reasonable value
-- (we don't have an Object_Subtype attribute). Consider:
-- subtype R is Character;
-- for R'Object_Size use 16;
-- If we inherit the alignment of 1, then we have an inefficient
-- alignment for the subtype, which cannot be fixed.
-- So we make the decision that if Size (or Object_Size) is given
-- (and, in the case of a first subtype, the alignment is not set
-- with a specific alignment clause), we reset the alignment to
-- the appropriate value for the specified size. This is a nice
-- simple rule to implement and document.
-- There is one slight glitch, which is that a confirming size
-- clause can now change the alignment, which, if we really think
-- that confirming rep clauses should have no effect, is a no-no.
-- type R is new Character;
-- for R'Alignment use 2;
-- type S is new R;
-- for S'Size use Character'Size;
-- Now the alignment of S is changed to 1 instead of 2 as a result
-- of applying the above rule to the confirming rep clause for S.
-- Not clear this is worth worrying about. If we recorded whether
-- a size clause was confirming we could avoid this, but right now
-- we have no way of doing that or easily figuring it out, so we
-- don't bother.
-- Historical note: in versions of GNAT prior to Nov 6th, 2011, an
-- odd distinction was made between inherited alignments larger
-- than the computed alignment (where the larger alignment was
-- inherited) and inherited alignments smaller than the computed
-- alignment (where the smaller alignment was overridden). This
-- was a dubious fix to get around an ACATS problem which seems
-- to have disappeared anyway, and in any case, this peculiarity
-- was never documented.
Init_Alignment (E, A);
-- If no Size (or Object_Size) was specified, then we inherited the
-- object size, so we should inherit the alignment as well and not
-- modify it. This takes care of cases like:
-- type R is new Integer;
-- for R'Alignment use 1;
-- subtype S is R;
-- Here we have R with a default Object_Size of 32, and a specified
-- alignment of 1, and it seeems right for S to inherit both values.
else
null;
-- Now we come to the difficult cases of subtypes for which we
-- have inherited an alignment different from the computed one.
-- We resort to the presence of alignment and size clauses to
-- guide our choices. Note that they can generally be present
-- only on the first subtype (except for Object_Size) and that
-- we need to look at the Rep_Item chain to correctly handle
-- derived types.
declare
FST : constant Entity_Id := First_Subtype (E);
function Has_Attribute_Clause
(E : Entity_Id;
Id : Attribute_Id) return Boolean;
-- Wrapper around Get_Attribute_Definition_Clause which tests
-- for the presence of the specified attribute clause.
--------------------------
-- Has_Attribute_Clause --
--------------------------
function Has_Attribute_Clause
(E : Entity_Id;
Id : Attribute_Id) return Boolean is
begin
return Present (Get_Attribute_Definition_Clause (E, Id));
end Has_Attribute_Clause;
begin
-- If the alignment comes from a clause, then we respect it.
-- Consider for example:
-- type R is new Character;
-- for R'Alignment use 1;
-- for R'Size use 16;
-- subtype S is R;
-- Here R has a specified size of 16 and a specified alignment
-- of 1, and it seems right for S to inherit both values.
if Has_Attribute_Clause (FST, Attribute_Alignment) then
null;
-- Now we come to the cases where we have inherited alignment
-- and size, and overridden the size but not the alignment.
elsif Has_Attribute_Clause (FST, Attribute_Size)
or else Has_Attribute_Clause (FST, Attribute_Object_Size)
or else Has_Attribute_Clause (E, Attribute_Object_Size)
then
-- This is tricky, it might be thought that we should try to
-- inherit the alignment, since that's what the RM implies,
-- but that leads to complex rules and oddities. Consider
-- for example:
-- type R is new Character;
-- for R'Size use 16;
-- It seems quite bogus in this case to inherit an alignment
-- of 1 from the parent type Character. Furthermore, if that
-- is what the programmer really wanted for some odd reason,
-- then he could specify the alignment directly.
-- Moreover we really don't want to inherit the alignment in
-- the case of a specified Object_Size for a subtype, since
-- there would be no way of overriding to give a reasonable
-- value (as we don't have an Object_Alignment attribute).
-- Consider for example:
-- subtype R is Character;
-- for R'Object_Size use 16;
-- If we inherit the alignment of 1, then it will be very
-- inefficient for the subtype and this cannot be fixed.
-- So we make the decision that if Size (or Object_Size) is
-- given and the alignment is not specified with a clause,
-- we reset the alignment to the appropriate value for the
-- specified size. This is a nice simple rule to implement
-- and document.
-- There is a theoretical glitch, which is that a confirming
-- size clause could now change the alignment, which, if we
-- really think that confirming rep clauses should have no
-- effect, could be seen as a no-no. However that's already
-- implemented by Alignment_Check_For_Size_Change so we do
-- not change the philosophy here.
-- Historical note: in versions prior to Nov 6th, 2011, an
-- odd distinction was made between inherited alignments
-- larger than the computed alignment (where the larger
-- alignment was inherited) and inherited alignments smaller
-- than the computed alignment (where the smaller alignment
-- was overridden). This was a dubious fix to get around an
-- ACATS problem which seems to have disappeared anyway, and
-- in any case, this peculiarity was never documented.
Init_Alignment (E, A);
-- If no Size (or Object_Size) was specified, then we have
-- inherited the object size, so we should also inherit the
-- alignment and not modify it.
else
null;
end if;
end;
end if;
end;
end Set_Elem_Alignment;

49
gcc/ada/sem_ch4.adb
View File

@ -4657,21 +4657,44 @@ package body Sem_Ch4 is
end loop;
-- If the scope is a current instance, the prefix cannot be an
-- expression of the same type (that would represent an attempt
-- to reach an internal operation of another synchronized object).
-- expression of the same type, unless the selector designates a
-- public operation (otherwise that would represent an attempt to
-- reach an internal entity of another synchronized object).
-- This is legal if prefix is an access to such type and there is
-- a dereference.
-- a dereference, or is a component with a dereferenced prefix.
if In_Scope
and then not Is_Entity_Name (Name)
and then Nkind (Name) /= N_Explicit_Dereference
then
Error_Msg_NE
("invalid reference to internal operation of some object of "
& "type &", N, Type_To_Use);
Set_Entity (Sel, Any_Id);
Set_Etype (Sel, Any_Type);
return;
if In_Scope and then not Is_Entity_Name (Name) then
declare
function Has_Dereference (N : Node_Id) return Boolean;
-- Check whether prefix includes a dereference at any level.
---------------------
-- Has_Dereference --
---------------------
function Has_Dereference (N : Node_Id) return Boolean is
begin
if Nkind (N) = N_Explicit_Dereference then
return True;
elsif
Nkind_In (N, N_Selected_Component, N_Indexed_Component)
then
return Has_Dereference (Prefix (N));
else
return False;
end if;
end Has_Dereference;
begin
if not Has_Dereference (Name) then
Error_Msg_NE ("invalid reference to internal operation "
& "of some object of type &", N, Type_To_Use);
Set_Entity (Sel, Any_Id);
Set_Etype (Sel, Any_Type);
return;
end if;
end;
end if;
-- If there is no visible entity with the given name or none of the

17
gcc/ada/sem_ch6.adb
View File

@ -3761,15 +3761,7 @@ package body Sem_Ch6 is
end if;
-- When generating code, inherited pre/postconditions are handled when
-- expanding the corresponding contract. In GNATprove the annotations
-- must be processed when the body is analyzed.
if GNATprove_Mode
and then Present (Spec_Id)
and then Present (Overridden_Operation (Spec_Id))
then
Collect_Inherited_Class_Wide_Conditions (Spec_Id, N);
end if;
-- expanding the corresponding contract.
-- Ada 2005 (AI-262): In library subprogram bodies, after the analysis
-- of the specification we have to install the private withed units.
@ -9946,6 +9938,13 @@ package body Sem_Ch6 is
Set_Convention (S, Convention (E));
Check_Dispatching_Operation (S, E);
-- In GNATprove_Mode, create the pragmas corresponding
-- to inherited class-wide conditions.
if GNATprove_Mode then
Collect_Inherited_Class_Wide_Conditions (S);
end if;
else
Check_Dispatching_Operation (S, Empty);
end if;

33
gcc/ada/sem_prag.adb
View File

@ -26759,17 +26759,18 @@ package body Sem_Prag is
-- Collect_Inherited_Class_Wide_Conditions --
---------------------------------------------
procedure Collect_Inherited_Class_Wide_Conditions
(Subp : Entity_Id;
Bod : Node_Id)
is
procedure Collect_Inherited_Class_Wide_Conditions (Subp : Entity_Id) is
Parent_Subp : constant Entity_Id := Overridden_Operation (Subp);
Prags : constant Node_Id := Contract (Parent_Subp);
Prag : Node_Id;
New_Prag : Node_Id;
Installed : Boolean;
begin
-- Iterate over the contract to find inherited class-wide pre- and
-- postconditions.
Installed := False;
-- Iterate over the contract of the overridden subprogram to find
-- inherited class-wide pre- and postconditions.
if Present (Prags) then
Prag := Pre_Post_Conditions (Prags);
@ -26777,17 +26778,29 @@ package body Sem_Prag is
while Present (Prag) loop
if Nam_In (Pragma_Name (Prag), Name_Precondition,
Name_Postcondition)
and then Class_Present (Prag)
then
if No (Declarations (Bod)) then
Set_Declarations (Bod, Empty_List);
-- The generated pragma must be analyzed in the context of
-- the subprogram, to make its formals visible.
if not Installed then
Installed := True;
Push_Scope (Subp);
Install_Formals (Subp);
end if;
Append_To (Declarations (Bod),
Build_Pragma_Check_Equivalent (Prag, Subp, Parent_Subp));
New_Prag :=
Build_Pragma_Check_Equivalent (Prag, Subp, Parent_Subp);
Insert_After (Unit_Declaration_Node (Subp), New_Prag);
Preanalyze (New_Prag);
end if;
Prag := Next_Pragma (Prag);
end loop;
if Installed then
End_Scope;
end if;
end if;
end Collect_Inherited_Class_Wide_Conditions;

12
gcc/ada/sem_prag.ads
View File

@ -311,12 +311,12 @@ package Sem_Prag is
-- state, variable or package instantiation denoted by Item_Id requires the
-- use of indicator/option Part_Of. If this is the case, emit an error.
procedure Collect_Inherited_Class_Wide_Conditions
(Subp : Entity_Id;
Bod : Node_Id);
-- When analyzing an overriding subprogram, check whether the overridden
-- operations have class-wide pre/postconditions, and generate the
-- corresponding pragmas.
procedure Collect_Inherited_Class_Wide_Conditions (Subp : Entity_Id);
-- In GNATprove mode, when analyzing an overriding subprogram, check
-- whether the overridden operations have class-wide pre/postconditions,
-- and generate the corresponding pragmas. The pragmas are inserted after
-- the subprogram declaration, together with those generated for other
-- aspects of the subprogram.
procedure Collect_Subprogram_Inputs_Outputs
(Subp_Id : Entity_Id;

20
gcc/ada/spark_xrefs.ads
View File

@ -209,9 +209,10 @@ package SPARK_Xrefs is
-- The following table records SPARK cross-references
type Xref_Index is new Int;
type Xref_Index is new Nat;
-- Used to index values in this table. Values start at 1 and are assigned
-- sequentially as entries are constructed.
-- sequentially as entries are constructed; value 0 is used temporarily
-- until a proper value is determined.
type SPARK_Xref_Record is record
Entity_Name : String_Ptr;
@ -268,9 +269,11 @@ package SPARK_Xrefs is
-- This table keeps track of the scopes and the corresponding starting and
-- ending indexes (From, To) in the Xref table.
type Scope_Index is new Int;
type Scope_Index is new Nat;
-- Used to index values in this table. Values start at 1 and are assigned
-- sequentially as entries are constructed.
-- sequentially as entries are constructed; value 0 indicates that no
-- entries have been constructed and is also used until a proper value is
-- determined.
type SPARK_Scope_Record is record
Scope_Name : String_Ptr;
@ -296,8 +299,10 @@ package SPARK_Xrefs is
Stype : Character;
-- Indicates type of scope, using code used in ALI file:
-- K = package
-- V = function
-- T = task
-- U = procedure
-- V = function
-- Y = entry
Col : Nat;
-- Column number for the scope
@ -329,9 +334,10 @@ package SPARK_Xrefs is
-- This table keeps track of the units and the corresponding starting and
-- ending indexes (From, To) in the Scope table.
type File_Index is new Int;
type File_Index is new Nat;
-- Used to index values in this table. Values start at 1 and are assigned
-- sequentially as entries are constructed.
-- sequentially as entries are constructed; value 0 indicates that no
-- entries have been constructed.
type SPARK_File_Record is record
File_Name : String_Ptr;

4
gcc/ada/targparm.ads
View File

@ -261,7 +261,7 @@ package Targparm is
-- Back-End Setjmp/Longjmp Exceptions
-- With this approach, the back end also handles the generation and
-- handling of exceptions, using setjmp/longjmp to setup receivers and
-- handling of exceptions, using setjmp/longjmp to set up receivers and
-- propagate. AT-END actions on exceptional paths are also taken care
-- of by the back end and the front end doesn't need to generate
-- explicit exception handlers for these.
@ -271,7 +271,7 @@ package Targparm is
-- The following switches specify whether we're using a front-end or a
-- back-end mechanism and whether this is a zero-cost or a sjlj scheme.
-- The per switch default values correspond to the default value of
-- The per-switch default values correspond to the default value of
-- Opt.Exception_Mechanism.
ZCX_By_Default_On_Target : Boolean := False;