+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
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.
+ else
+ -- 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.
- Init_Alignment (E, A);
+ declare
+ FST : constant Entity_Id := First_Subtype (E);
- -- 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:
+ 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.
- -- type R is new Integer;
- -- for R'Alignment use 1;
- -- subtype S is R;
+ --------------------------
+ -- Has_Attribute_Clause --
+ --------------------------
- -- 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.
+ 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;
- else
- null;
+ 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;
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
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.
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;
-- 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);
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;
-- 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;
-- 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;
-- 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;
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
-- 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;
-- 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.
-- 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;
projects / gcc.git / commitdiff