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
with Entity_Id of the reference.
* spark_xrefs.adb (dspark): Adapt pretty-printing routine.
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;