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

lib-xref-spark_specific.adb (Add_SPARK_Xrefs): Remove special-case for constants (with variable input).

Browse Source 
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
This commit is contained in:
Pierre-Marie de Rodat 2017-11-08 16:45:55 +00:00
parent 2cf8eabd48
commit 9ac3cbb39d
11 changed files with 140 additions and 91 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

25
gcc/ada/ChangeLog
View File

@ -1,3 +1,28 @@
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

10
gcc/ada/exp_ch9.adb
View File

@ -12909,8 +12909,8 @@ package body Exp_Ch9 is
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 :=
@ -14590,9 +14590,9 @@ package body Exp_Ch9 is
-- 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,

66
gcc/ada/lib-xref-spark_specific.adb
View File

@ -252,11 +252,6 @@ package body SPARK_Specific is
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;
@ -332,50 +327,6 @@ package body SPARK_Specific is
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 --
----------------------------
@ -729,7 +680,6 @@ package body SPARK_Specific is
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
@ -757,24 +707,10 @@ package body SPARK_Specific 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;

36
gcc/ada/sem_ch4.adb
View File

@ -414,12 +414,44 @@ package body Sem_Ch4 is
-----------------------
-- 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;

10
gcc/ada/sem_disp.adb
View File

@ -2371,9 +2371,9 @@ package body Sem_Disp is
-----------------------------------
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
@ -2386,9 +2386,11 @@ package body Sem_Disp is
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;

12
gcc/ada/sem_res.adb
View File

@ -2439,13 +2439,11 @@ package body Sem_Res is
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

10
gcc/ada/sem_util.adb
View File

@ -597,6 +597,7 @@ package body Sem_Util is
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
@ -13198,14 +13199,14 @@ package body Sem_Util is
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;
@ -23329,6 +23330,7 @@ package body Sem_Util is
declare
H : Entity_Id := Homonym (N);
Nr : Nat := 1;
begin
while Present (H) loop
if Scope (H) = Scope (N) then

6
gcc/ada/spark_xrefs.adb
View File

@ -39,7 +39,7 @@ package body SPARK_Xrefs is
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);
@ -62,7 +62,7 @@ package body SPARK_Xrefs is
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);
@ -92,7 +92,7 @@ package body SPARK_Xrefs is
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);

1
gcc/ada/spark_xrefs.ads
View File

@ -75,7 +75,6 @@ package SPARK_Xrefs is
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;

4
gcc/testsuite/ChangeLog
View File

@ -1,3 +1,7 @@
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

51
gcc/testsuite/gnat.dg/delta_aggr.adb Normal file
View File

@ -0,0 +1,51 @@
-- { 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;