gcc/ada/
2017-11-08 Piotr Trojanek <trojanek@adacore.com>
* lib-xref-spark_specific.adb (Add_SPARK_Xrefs): Remove special-case
for constants (with variable input).
(Is_Constant_Object_Without_Variable_Input): Remove.
2017-11-08 Hristian Kirtchev <kirtchev@adacore.com>
* exp_ch9.adb, sem_disp.adb, sem_util.adb: Minor reformatting.
2017-11-08 Piotr Trojanek <trojanek@adacore.com>
* spark_xrefs.ads (Rtype): Remove special-casing of constants for SPARK
cross-references.
(dspark): Remove hardcoded table bound.
2017-11-08 Ed Schonberg <schonberg@adacore.com>
* sem_ch4.adb (Analyze_Aggregate): For
Ada2020 delta aggregates, use
the type of the base of the construct to determine the type (or
candidate interpretations) of the delta aggregate. This allows the
construct to appear in a context that expects a private extension.
* sem_res.adb (Resolve): Handle properly a delta aggregate with an
overloaded base.
gcc/testsuite/
2017-11-08 Ed Schonberg <schonberg@adacore.com>
* gnat.dg/delta_aggr.adb: New testcase.
From-SVN: r254544
+2017-11-08 Piotr Trojanek <trojanek@adacore.com>
+
+ * lib-xref-spark_specific.adb (Add_SPARK_Xrefs): Remove special-case
+ for constants (with variable input).
+ (Is_Constant_Object_Without_Variable_Input): Remove.
+
+2017-11-08 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * exp_ch9.adb, sem_disp.adb, sem_util.adb: Minor reformatting.
+
+2017-11-08 Piotr Trojanek <trojanek@adacore.com>
+
+ * spark_xrefs.ads (Rtype): Remove special-casing of constants for SPARK
+ cross-references.
+ (dspark): Remove hardcoded table bound.
+
+2017-11-08 Ed Schonberg <schonberg@adacore.com>
+
+ * sem_ch4.adb (Analyze_Aggregate): For Ada2020 delta aggregates, use
+ the type of the base of the construct to determine the type (or
+ candidate interpretations) of the delta aggregate. This allows the
+ construct to appear in a context that expects a private extension.
+ * sem_res.adb (Resolve): Handle properly a delta aggregate with an
+ overloaded base.
+
2017-11-08 Piotr Trojanek <trojanek@adacore.com>
* spark_xrefs.ads (SPARK_Xref_Record): Replace file and scope indices
end if;
-- If the type of the dispatching object is an access type then return
- -- an explicit dereference of a copy of the object, and note that
- -- this is the controlling actual of the call.
+ -- an explicit dereference of a copy of the object, and note that this
+ -- is the controlling actual of the call.
if Is_Access_Type (Etype (Object)) then
Object :=
-- Jnn'unchecked_access
- -- and add it to aggegate for access to formals. Note that
- -- the actual may be by-copy but still be a controlling actual
- -- if it is an access to class-wide interface.
+ -- and add it to aggegate for access to formals. Note that the
+ -- actual may be by-copy but still be a controlling actual if it
+ -- is an access to class-wide interface.
if not Is_Controlling_Actual (Actual) then
Append_To (Params,
function Get_Scope_Num (E : Entity_Id) return Nat;
-- Return the scope number associated with the entity E
- function Is_Constant_Object_Without_Variable_Input
- (E : Entity_Id) return Boolean;
- -- Return True if E is known to have no variable input, as defined in
- -- SPARK RM.
-
function Is_Future_Scope_Entity
(E : Entity_Id;
S : Scope_Index) return Boolean;
function Get_Scope_Num (E : Entity_Id) return Nat renames Scopes.Get;
- -----------------------------------------------
- -- Is_Constant_Object_Without_Variable_Input --
- -----------------------------------------------
-
- function Is_Constant_Object_Without_Variable_Input
- (E : Entity_Id) return Boolean
- is
- begin
- case Ekind (E) is
-
- -- A constant is known to have no variable input if its
- -- initializing expression is static (a value which is
- -- compile-time-known is not guaranteed to have no variable input
- -- as defined in the SPARK RM). Otherwise, the constant may or not
- -- have variable input.
-
- when E_Constant =>
- declare
- Decl : Node_Id;
- begin
- if Present (Full_View (E)) then
- Decl := Parent (Full_View (E));
- else
- Decl := Parent (E);
- end if;
-
- if Is_Imported (E) then
- return False;
- else
- pragma Assert (Present (Expression (Decl)));
- return Is_Static_Expression (Expression (Decl));
- end if;
- end;
-
- when E_In_Parameter
- | E_Loop_Parameter
- =>
- return True;
-
- when others =>
- return False;
- end case;
- end Is_Constant_Object_Without_Variable_Input;
-
----------------------------
-- Is_Future_Scope_Entity --
----------------------------
declare
Ref_Entry : Xref_Entry renames Xrefs.Table (Rnums (Refno));
Ref : Xref_Key renames Ref_Entry.Key;
- Typ : Character;
begin
-- If this assertion fails, the scope which we are looking for is
pragma Assert (Scope_Id <= SPARK_Scope_Table.Last);
end loop;
- -- References to constant objects without variable inputs (see
- -- SPARK RM 3.3.1) are considered specially in SPARK section,
- -- because these will be translated as constants in the
- -- intermediate language for formal verification, and should
- -- therefore never appear in frame conditions. Other constants may
- -- later be treated the same, up to GNATprove to decide based on
- -- its flow analysis.
-
- if Is_Constant_Object_Without_Variable_Input (Ref.Ent) then
- Typ := 'c';
- else
- Typ := Ref.Typ;
- end if;
-
SPARK_Xref_Table.Append (
(Entity => Unique_Entity (Ref.Ent),
Ref_Scope => Ref.Ref_Scope,
- Rtype => Typ));
+ Rtype => Ref.Typ));
end;
end loop;
-----------------------
-- Most of the analysis of Aggregates requires that the type be known,
- -- and is therefore put off until resolution.
+ -- and is therefore put off until resolution of the context.
+ -- Delta aggregates have a base component that determines the type of the
+ -- enclosing aggregate so its type can be ascertained earlier. This also
+ -- allows delta aggregates to appear in the context of a record type with
+ -- a private extension, as per the latest update of AI2-0127.
procedure Analyze_Aggregate (N : Node_Id) is
begin
if No (Etype (N)) then
- Set_Etype (N, Any_Composite);
+ if Nkind (N) = N_Delta_Aggregate then
+ declare
+ Base : constant Node_Id := Expression (N);
+ I : Interp_Index;
+ It : Interp;
+
+ begin
+ Analyze (Base);
+
+ -- If the base is overloaded, propagate interpretations
+ -- to the enclosing aggregate.
+
+ if Is_Overloaded (Base) then
+ Get_First_Interp (Base, I, It);
+ Set_Etype (N, Any_Type);
+
+ while Present (It.Nam) loop
+ Add_One_Interp (N, It.Typ, It.Typ);
+ Get_Next_Interp (I, It);
+ end loop;
+
+ else
+ Set_Etype (N, Etype (Base));
+ end if;
+ end;
+
+ else
+ Set_Etype (N, Any_Composite);
+ end if;
end if;
end Analyze_Aggregate;
-----------------------------------
function Is_Inherited_Public_Operation (Op : Entity_Id) return Boolean is
+ Pack_Decl : Node_Id;
Prim : Entity_Id := Op;
Scop : Entity_Id := Prim;
- Pack_Decl : Node_Id;
begin
-- Locate the ultimate non-hidden alias entity
if Comes_From_Source (Prim) and then Ekind (Scop) = E_Package then
Pack_Decl := Unit_Declaration_Node (Scop);
- return Nkind (Pack_Decl) = N_Package_Declaration
- and then List_Containing (Unit_Declaration_Node (Prim)) =
- Visible_Declarations (Specification (Pack_Decl));
+
+ return
+ Nkind (Pack_Decl) = N_Package_Declaration
+ and then List_Containing (Unit_Declaration_Node (Prim)) =
+ Visible_Declarations (Specification (Pack_Decl));
else
return False;
Set_Entity (N, Seen);
Generate_Reference (Seen, N);
- elsif Nkind (N) = N_Case_Expression then
- Set_Etype (N, Expr_Type);
-
- elsif Nkind (N) = N_Character_Literal then
- Set_Etype (N, Expr_Type);
-
- elsif Nkind (N) = N_If_Expression then
+ elsif Nkind_In (N, N_Case_Expression,
+ N_Character_Literal,
+ N_If_Expression,
+ N_Delta_Aggregate)
+ then
Set_Etype (N, Expr_Type);
-- AI05-0139-2: Expression is overloaded because type has
procedure Inner (E : Entity_Id) is
Scop : Node_Id;
+
begin
-- If entity has an internal name, skip by it, and print its scope.
-- Note that we strip a final R from the name before the test; this
if Ekind (Proc_Nam) = E_Procedure
and then Present (Parameter_Specifications (Parent (Proc_Nam)))
then
- Param := Parameter_Type (First (
- Parameter_Specifications (Parent (Proc_Nam))));
+ Param :=
+ Parameter_Type
+ (First (Parameter_Specifications (Parent (Proc_Nam))));
- -- The formal may be an anonymous access type.
+ -- The formal may be an anonymous access type
if Nkind (Param) = N_Access_Definition then
Param_Typ := Entity (Subtype_Mark (Param));
-
else
Param_Typ := Etype (Param);
end if;
declare
H : Entity_Id := Homonym (N);
Nr : Nat := 1;
+
begin
while Present (H) loop
if Scope (H) = Scope (N) then
Write_Line ("SPARK Xrefs File Table");
Write_Line ("----------------------");
- for Index in 1 .. SPARK_File_Table.Last loop
+ for Index in SPARK_File_Table.First .. SPARK_File_Table.Last loop
declare
AFR : SPARK_File_Record renames SPARK_File_Table.Table (Index);
Write_Line ("SPARK Xrefs Scope Table");
Write_Line ("-----------------------");
- for Index in 1 .. SPARK_Scope_Table.Last loop
+ for Index in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
declare
ASR : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Index);
Write_Line ("SPARK Xref Table");
Write_Line ("----------------");
- for Index in 1 .. SPARK_Xref_Table.Last loop
+ for Index in SPARK_Xref_Table.First .. SPARK_Xref_Table.Last loop
declare
AXR : SPARK_Xref_Record renames SPARK_Xref_Table.Table (Index);
Rtype : Character;
-- Indicates type of the reference, using code used in ALI file:
-- r = reference
- -- c = reference to constant object
-- m = modification
-- s = call
end record;
+2017-11-08 Ed Schonberg <schonberg@adacore.com>
+
+ * gnat.dg/delta_aggr.adb: New testcase.
+
2017-11-08 Jakub Jelinek <jakub@redhat.com>
* g++.dg/pr57878.C (__sso_string_base::_M_get_allocator): Return
--- /dev/null
+-- { dg-do compile }
+-- { dg-options "-gnat2020" }
+
+procedure Delta_Aggr is
+ type T1 is tagged record
+ F1, F2, F3 : Integer := 0;
+ end record;
+
+ function Make (X : Integer) return T1 is
+ begin
+ return (10, 20, 30);
+ end Make;
+
+ package Pkg is
+ type T2 is new T1 with private;
+ X, Y : constant T2;
+ function Make (X : Integer) return T2;
+ private
+ type T2 is new T1 with
+ record
+ F4 : Integer := 0;
+ end record;
+ X : constant T2 := (0, 0, 0, 0);
+ Y : constant T2 := (1, 2, 0, 0);
+ end Pkg;
+
+ package body Pkg is
+ function Make (X : Integer) return T2 is
+ begin
+ return (X, X ** 2, X ** 3, X ** 4);
+ end Make;
+ end Pkg;
+
+ use Pkg;
+
+ Z : T2 := (Y with delta F1 => 111);
+
+ -- a legal delta aggregate whose type is a private extension
+ pragma Assert (Y = (X with delta F1 => 1, F2 => 2));
+ pragma assert (Y.F2 = X.F1);
+
+begin
+ Z := (X with delta F1 => 1);
+
+ -- The base of the delta aggregate can be overloaded, in which case
+ -- the candidate interpretations for the aggregate are those of the
+ -- base, to be resolved from context.
+
+ Z := (Make (2) with delta F1 => 1);
+ null;
+end Delta_Aggr;
git://gcc.gnu.org / gcc.git / commitdiff