Commit 54740d7d by Arnaud Charlet

[multiple changes]

2017-01-19  Javier Miranda  <miranda@adacore.com>

	* exp_aggr.adb (Pass_Aggregate_To_Back_End): Renamed as
	Build_Back_End_Aggregate.
	(Generate_Aggregate_For_Derived_Type): Code cleanup.
	(Prepend_Stored_Values): Code cleanup.

2017-01-19  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch6.adb (Analyze_Expression_Function): Check for an
	incomplete return type after attempting to freeze it, so that
	other freeze actiona are generated in the proper order.

2017-01-19  Ed Schonberg  <schonberg@adacore.com>

	* sem_aggr.adb (Resolve_Aggregate): If the type is a string
	type, ie. a type whose component is a character type, and the
	aggregate is positional, do not convert into a string literal
	if the index type is not an integer type, because the original
	type may be required in an enclosing operation.

2017-01-19  Bob Duff  <duff@adacore.com>

	* binde.adb, debug.adb: Enable new elaboration order algorithm
	by default. -dp switch reverts to the old algorithm.

2017-01-19  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_ch3.adb Add with and use clauses for Exp_Ch7.
	(Analyze_Declarations): Create the DIC and Invariant
	procedure bodies s after all freezing has taken place.
	(Build_Assertion_Bodies): New routine.
	* sem_ch7.adb Remove the with and use clauses for Exp_Ch7
	and Exp_Util.
	(Analyze_Package_Specification): Remove the
	generation of the DIC and Invariant procedure bodies. This is
	now done by Analyze_Declarations.
	* sem_disp.adb (Check_Dispatching_Operation): DIC and Invariant
	procedures are never treated as primitives.

2017-01-19  Yannick Moy  <moy@adacore.com>

	* frontend.adb: Analyze inlined bodies and check elaboration
	rules in GNATprove mode too.
	* sem_elab.adb (Delay_Element): Add Boolean component to save
	indication that call is in SPARK code.	(Check_Elab_Calls):
	Check elaboration rules in GNATprove mode, and correctly set
	the current value of SPARK_Mode.
	* lib-xref-spark_specific.adb
	(Add_SPARK_Xrefs): Simplify iteration over dereferences.

2017-01-19  Ed Schonberg  <schonberg@adacore.com>

	* exp_ch4.adb (Expand_Concatenate): Do no enable overflow
	checks on the expression for the high bound of concatenation
	when checks are disabled, to suppress warnings about potential
	constraint errors in restricted runtimes.

From-SVN: r244626
parent 138fc6f1
2017-01-19 Javier Miranda <miranda@adacore.com>
* exp_aggr.adb (Pass_Aggregate_To_Back_End): Renamed as
Build_Back_End_Aggregate.
(Generate_Aggregate_For_Derived_Type): Code cleanup.
(Prepend_Stored_Values): Code cleanup.
2017-01-19 Ed Schonberg <schonberg@adacore.com>
* sem_ch6.adb (Analyze_Expression_Function): Check for an
incomplete return type after attempting to freeze it, so that
other freeze actiona are generated in the proper order.
2017-01-19 Ed Schonberg <schonberg@adacore.com>
* sem_aggr.adb (Resolve_Aggregate): If the type is a string
type, ie. a type whose component is a character type, and the
aggregate is positional, do not convert into a string literal
if the index type is not an integer type, because the original
type may be required in an enclosing operation.
2017-01-19 Bob Duff <duff@adacore.com>
* binde.adb, debug.adb: Enable new elaboration order algorithm
by default. -dp switch reverts to the old algorithm.
2017-01-19 Hristian Kirtchev <kirtchev@adacore.com>
* sem_ch3.adb Add with and use clauses for Exp_Ch7.
(Analyze_Declarations): Create the DIC and Invariant
procedure bodies s after all freezing has taken place.
(Build_Assertion_Bodies): New routine.
* sem_ch7.adb Remove the with and use clauses for Exp_Ch7
and Exp_Util.
(Analyze_Package_Specification): Remove the
generation of the DIC and Invariant procedure bodies. This is
now done by Analyze_Declarations.
* sem_disp.adb (Check_Dispatching_Operation): DIC and Invariant
procedures are never treated as primitives.
2017-01-19 Yannick Moy <moy@adacore.com>
* frontend.adb: Analyze inlined bodies and check elaboration
rules in GNATprove mode too.
* sem_elab.adb (Delay_Element): Add Boolean component to save
indication that call is in SPARK code. (Check_Elab_Calls):
Check elaboration rules in GNATprove mode, and correctly set
the current value of SPARK_Mode.
* lib-xref-spark_specific.adb
(Add_SPARK_Xrefs): Simplify iteration over dereferences.
2017-01-19 Ed Schonberg <schonberg@adacore.com>
* exp_ch4.adb (Expand_Concatenate): Do no enable overflow
checks on the expression for the high bound of concatenation
when checks are disabled, to suppress warnings about potential
constraint errors in restricted runtimes.
2017-01-19 Hristian Kirtchev <kirtchev@adacore.com>
* exp_ch3.adb (Expand_Freeze_Enumeration_Type): Mark the
......
......@@ -37,8 +37,7 @@ with System.OS_Lib;
package body Binde is
-- We now have Elab_New, a new elaboration-order algorithm. It has the
-- property that ???
-- We now have Elab_New, a new elaboration-order algorithm.
--
-- However, any change to elaboration order can break some programs.
-- Therefore, we are keeping the old algorithm in place, to be selected
......@@ -289,7 +288,12 @@ package body Binde is
function Debug_Flag_Older return Boolean;
function Debug_Flag_Old return Boolean;
-- True if debug flags select the old or older algorithms
-- True if debug flags select the old or older algorithms. Pretty much any
-- change to elaboration order can break some programs. For example,
-- programs can depend on elaboration order even without failing
-- access-before-elaboration checks. A trivial example is a program that
-- prints text during elaboration. Therefore, we have flags to revert to
-- the old(er) algorithms.
procedure Validate (Order : Unit_Id_Array; Doing_New : Boolean);
-- Assert that certain properties are true
......@@ -1134,10 +1138,7 @@ package body Binde is
function Debug_Flag_Old return Boolean is
begin
-- For now, Debug_Flag_P means "use the new algorithm". Once it is
-- stable, we intend to remove the "not" below.
return not Debug_Flag_P;
return Debug_Flag_P;
end Debug_Flag_Old;
----------------------
......
......@@ -182,7 +182,7 @@ package body Debug is
-- dm
-- dn List details of manipulation of Num_Pred values
-- do Use older preference for elaboration order
-- dp Use new preference for elaboration order
-- dp Use old preference for elaboration order
-- dq
-- dr
-- ds
......@@ -813,16 +813,15 @@ package body Debug is
-- prefer specs with no bodies to specs with bodies, and between two
-- specs with bodies, prefers the one whose body is closer to being
-- able to be elaborated. This is a clear improvement, but we provide
-- this debug flag in case of regressions.
-- this debug flag in case of regressions. Note: -do is even older than
-- -dp.
-- dp Use new elaboration order preference. The new preference rules
-- dp Use old elaboration order preference. The new preference rules
-- elaborate all units within a strongly connected component together,
-- with no other units in between. In particular, if a spec/body pair
-- can be elaborated together, it will be. In the new order, the binder
-- behaves as if every pragma Elaborate_All that would be legal is
-- present, even if it does not appear in the source code. NOTE: We
-- intend to reverse the sense of this switch at some point, so the new
-- preference is the default.
-- present, even if it does not appear in the source code.
-- du List unit name and file name for each unit as it is read in
......
......@@ -6507,6 +6507,9 @@ package body Exp_Aggr is
-- and the aggregate can be constructed statically and handled by
-- the back-end.
procedure Build_Back_End_Aggregate;
-- Build a proper aggregate to be handled by the back-end
function Compile_Time_Known_Composite_Value (N : Node_Id) return Boolean;
-- Returns true if N is an expression of composite type which can be
-- fully evaluated at compile time without raising constraint error.
......@@ -6545,192 +6548,15 @@ package body Exp_Aggr is
-- because it will not be set when type and its parent are in the
-- same scope, and the parent component needs expansion.
procedure Pass_Aggregate_To_Back_End;
-- Build a proper aggregate to be handled by the back-end
function Top_Level_Aggregate (N : Node_Id) return Node_Id;
-- For nested aggregates return the ultimate enclosing aggregate; for
-- non-nested aggregates return N.
----------------------------------------
-- Compile_Time_Known_Composite_Value --
----------------------------------------
function Compile_Time_Known_Composite_Value
(N : Node_Id) return Boolean
is
begin
-- If we have an entity name, then see if it is the name of a
-- constant and if so, test the corresponding constant value.
if Is_Entity_Name (N) then
declare
E : constant Entity_Id := Entity (N);
V : Node_Id;
begin
if Ekind (E) /= E_Constant then
return False;
else
V := Constant_Value (E);
return Present (V)
and then Compile_Time_Known_Composite_Value (V);
end if;
end;
-- We have a value, see if it is compile time known
else
if Nkind (N) = N_Aggregate then
return Compile_Time_Known_Aggregate (N);
end if;
-- All other types of values are not known at compile time
return False;
end if;
end Compile_Time_Known_Composite_Value;
------------------------------
-- Build_Back_End_Aggregate --
------------------------------
----------------------------------
-- Component_Not_OK_For_Backend --
----------------------------------
function Component_Not_OK_For_Backend return Boolean is
C : Node_Id;
Expr_Q : Node_Id;
begin
if No (Comps) then
return False;
end if;
C := First (Comps);
while Present (C) loop
-- If the component has box initialization, expansion is needed
-- and component is not ready for backend.
if Box_Present (C) then
return True;
end if;
if Nkind (Expression (C)) = N_Qualified_Expression then
Expr_Q := Expression (Expression (C));
else
Expr_Q := Expression (C);
end if;
-- Return true if the aggregate has any associations for tagged
-- components that may require tag adjustment.
-- These are cases where the source expression may have a tag that
-- could differ from the component tag (e.g., can occur for type
-- conversions and formal parameters). (Tag adjustment not needed
-- if Tagged_Type_Expansion because object tags are implicit in
-- the machine.)
if Is_Tagged_Type (Etype (Expr_Q))
and then (Nkind (Expr_Q) = N_Type_Conversion
or else (Is_Entity_Name (Expr_Q)
and then
Ekind (Entity (Expr_Q)) in Formal_Kind))
and then Tagged_Type_Expansion
then
Static_Components := False;
return True;
elsif Is_Delayed_Aggregate (Expr_Q) then
Static_Components := False;
return True;
elsif Possible_Bit_Aligned_Component (Expr_Q) then
Static_Components := False;
return True;
elsif Modify_Tree_For_C
and then Nkind (C) = N_Component_Association
and then Has_Per_Object_Constraint (Choices (C))
then
Static_Components := False;
return True;
elsif Modify_Tree_For_C
and then Nkind (Expr_Q) = N_Identifier
and then Is_Array_Type (Etype (Expr_Q))
then
Static_Components := False;
return True;
end if;
if Is_Elementary_Type (Etype (Expr_Q)) then
if not Compile_Time_Known_Value (Expr_Q) then
Static_Components := False;
end if;
elsif not Compile_Time_Known_Composite_Value (Expr_Q) then
Static_Components := False;
if Is_Private_Type (Etype (Expr_Q))
and then Has_Discriminants (Etype (Expr_Q))
then
return True;
end if;
end if;
Next (C);
end loop;
return False;
end Component_Not_OK_For_Backend;
-------------------------------
-- Has_Per_Object_Constraint --
-------------------------------
function Has_Per_Object_Constraint (L : List_Id) return Boolean is
N : Node_Id := First (L);
begin
while Present (N) loop
if Is_Entity_Name (N)
and then Present (Entity (N))
and then Has_Per_Object_Constraint (Entity (N))
then
return True;
end if;
Next (N);
end loop;
return False;
end Has_Per_Object_Constraint;
-----------------------------------
-- Has_Visible_Private_Ancestor --
-----------------------------------
function Has_Visible_Private_Ancestor (Id : E) return Boolean is
R : constant Entity_Id := Root_Type (Id);
T1 : Entity_Id := Id;
begin
loop
if Is_Private_Type (T1) then
return True;
elsif T1 = R then
return False;
else
T1 := Etype (T1);
end if;
end loop;
end Has_Visible_Private_Ancestor;
--------------------------------
-- Pass_Aggregate_To_Back_End --
--------------------------------
procedure Pass_Aggregate_To_Back_End is
procedure Build_Back_End_Aggregate is
Comp : Entity_Id;
New_Comp : Node_Id;
Tag_Value : Node_Id;
......@@ -6761,13 +6587,6 @@ package body Exp_Aggr is
-- describe the type and its components.
Generate_Aggregate_For_Derived_Type : declare
Constraints : constant List_Id := New_List;
First_Comp : Node_Id;
Discriminant : Entity_Id;
Decl : Node_Id;
Num_Disc : Nat := 0;
Num_Gird : Nat := 0;
procedure Prepend_Stored_Values (T : Entity_Id);
-- Scan the list of stored discriminants of the type, and add
-- their values to the aggregate being built.
......@@ -6777,17 +6596,20 @@ package body Exp_Aggr is
---------------------------
procedure Prepend_Stored_Values (T : Entity_Id) is
Discr : Entity_Id;
First_Comp : Node_Id := Empty;
begin
Discriminant := First_Stored_Discriminant (T);
while Present (Discriminant) loop
Discr := First_Stored_Discriminant (T);
while Present (Discr) loop
New_Comp :=
Make_Component_Association (Loc,
Choices => New_List (
New_Occurrence_Of (Discriminant, Loc)),
New_Occurrence_Of (Discr, Loc)),
Expression =>
New_Copy_Tree
(Get_Discriminant_Value
(Discriminant,
(Discr,
Typ,
Discriminant_Constraint (Typ))));
......@@ -6798,26 +6620,41 @@ package body Exp_Aggr is
end if;
First_Comp := New_Comp;
Next_Stored_Discriminant (Discriminant);
Next_Stored_Discriminant (Discr);
end loop;
end Prepend_Stored_Values;
-- Local variables
Constraints : constant List_Id := New_List;
Discr : Entity_Id;
Decl : Node_Id;
Num_Disc : Nat := 0;
Num_Gird : Nat := 0;
-- Start of processing for Generate_Aggregate_For_Derived_Type
begin
-- Remove the associations for the discriminant of derived type
First_Comp := First (Component_Associations (N));
while Present (First_Comp) loop
Comp := First_Comp;
Next (First_Comp);
declare
First_Comp : Node_Id;
if Ekind (Entity (First (Choices (Comp)))) = E_Discriminant
then
Remove (Comp);
Num_Disc := Num_Disc + 1;
end if;
end loop;
begin
First_Comp := First (Component_Associations (N));
while Present (First_Comp) loop
Comp := First_Comp;
Next (First_Comp);
if Ekind (Entity (First (Choices (Comp)))) =
E_Discriminant
then
Remove (Comp);
Num_Disc := Num_Disc + 1;
end if;
end loop;
end;
-- Insert stored discriminant associations in the correct
-- order. If there are more stored discriminants than new
......@@ -6828,12 +6665,10 @@ package body Exp_Aggr is
-- components. Otherwise there is one-one correspondence
-- between the constraints and the stored discriminants.
First_Comp := Empty;
Discriminant := First_Stored_Discriminant (Base_Type (Typ));
while Present (Discriminant) loop
Discr := First_Stored_Discriminant (Base_Type (Typ));
while Present (Discr) loop
Num_Gird := Num_Gird + 1;
Next_Stored_Discriminant (Discriminant);
Next_Stored_Discriminant (Discr);
end loop;
-- Case of more stored discriminants than new discriminants
......@@ -6844,17 +6679,17 @@ package body Exp_Aggr is
-- proper implementation type for the aggregate, and convert
-- it to the intended target type.
Discriminant := First_Stored_Discriminant (Base_Type (Typ));
while Present (Discriminant) loop
Discr := First_Stored_Discriminant (Base_Type (Typ));
while Present (Discr) loop
New_Comp :=
New_Copy_Tree
(Get_Discriminant_Value
(Discriminant,
(Discr,
Typ,
Discriminant_Constraint (Typ)));
Append (New_Comp, Constraints);
Next_Stored_Discriminant (Discriminant);
Next_Stored_Discriminant (Discr);
end loop;
Decl :=
......@@ -6920,8 +6755,8 @@ package body Exp_Aggr is
Append_To (Comps,
Make_Component_Association (Loc,
Choices =>
New_List (New_Occurrence_Of (Comp, Loc)),
Choices => New_List (
New_Occurrence_Of (Comp, Loc)),
Expression => New_Comp));
Analyze_And_Resolve (New_Comp, Etype (Comp));
......@@ -6937,8 +6772,10 @@ package body Exp_Aggr is
if Present (Orig_Tag) then
Tag_Value := Orig_Tag;
elsif not Tagged_Type_Expansion then
Tag_Value := Empty;
else
Tag_Value :=
New_Occurrence_Of
......@@ -6959,7 +6796,7 @@ package body Exp_Aggr is
-- Remove the inherited component association from the
-- aggregate and store them in the parent aggregate
First_Comp := First (Component_Associations (N));
First_Comp := First (Component_Associations (N));
Parent_Comps := New_List;
while Present (First_Comp)
and then
......@@ -7028,7 +6865,181 @@ package body Exp_Aggr is
end;
end if;
end if;
end Pass_Aggregate_To_Back_End;
end Build_Back_End_Aggregate;
----------------------------------------
-- Compile_Time_Known_Composite_Value --
----------------------------------------
function Compile_Time_Known_Composite_Value
(N : Node_Id) return Boolean
is
begin
-- If we have an entity name, then see if it is the name of a
-- constant and if so, test the corresponding constant value.
if Is_Entity_Name (N) then
declare
E : constant Entity_Id := Entity (N);
V : Node_Id;
begin
if Ekind (E) /= E_Constant then
return False;
else
V := Constant_Value (E);
return Present (V)
and then Compile_Time_Known_Composite_Value (V);
end if;
end;
-- We have a value, see if it is compile time known
else
if Nkind (N) = N_Aggregate then
return Compile_Time_Known_Aggregate (N);
end if;
-- All other types of values are not known at compile time
return False;
end if;
end Compile_Time_Known_Composite_Value;
----------------------------------
-- Component_Not_OK_For_Backend --
----------------------------------
function Component_Not_OK_For_Backend return Boolean is
C : Node_Id;
Expr_Q : Node_Id;
begin
if No (Comps) then
return False;
end if;
C := First (Comps);
while Present (C) loop
-- If the component has box initialization, expansion is needed
-- and component is not ready for backend.
if Box_Present (C) then
return True;
end if;
if Nkind (Expression (C)) = N_Qualified_Expression then
Expr_Q := Expression (Expression (C));
else
Expr_Q := Expression (C);
end if;
-- Return true if the aggregate has any associations for tagged
-- components that may require tag adjustment.
-- These are cases where the source expression may have a tag that
-- could differ from the component tag (e.g., can occur for type
-- conversions and formal parameters). (Tag adjustment not needed
-- if Tagged_Type_Expansion because object tags are implicit in
-- the machine.)
if Is_Tagged_Type (Etype (Expr_Q))
and then (Nkind (Expr_Q) = N_Type_Conversion
or else (Is_Entity_Name (Expr_Q)
and then
Ekind (Entity (Expr_Q)) in Formal_Kind))
and then Tagged_Type_Expansion
then
Static_Components := False;
return True;
elsif Is_Delayed_Aggregate (Expr_Q) then
Static_Components := False;
return True;
elsif Possible_Bit_Aligned_Component (Expr_Q) then
Static_Components := False;
return True;
elsif Modify_Tree_For_C
and then Nkind (C) = N_Component_Association
and then Has_Per_Object_Constraint (Choices (C))
then
Static_Components := False;
return True;
elsif Modify_Tree_For_C
and then Nkind (Expr_Q) = N_Identifier
and then Is_Array_Type (Etype (Expr_Q))
then
Static_Components := False;
return True;
end if;
if Is_Elementary_Type (Etype (Expr_Q)) then
if not Compile_Time_Known_Value (Expr_Q) then
Static_Components := False;
end if;
elsif not Compile_Time_Known_Composite_Value (Expr_Q) then
Static_Components := False;
if Is_Private_Type (Etype (Expr_Q))
and then Has_Discriminants (Etype (Expr_Q))
then
return True;
end if;
end if;
Next (C);
end loop;
return False;
end Component_Not_OK_For_Backend;
-------------------------------
-- Has_Per_Object_Constraint --
-------------------------------
function Has_Per_Object_Constraint (L : List_Id) return Boolean is
N : Node_Id := First (L);
begin
while Present (N) loop
if Is_Entity_Name (N)
and then Present (Entity (N))
and then Has_Per_Object_Constraint (Entity (N))
then
return True;
end if;
Next (N);
end loop;
return False;
end Has_Per_Object_Constraint;
-----------------------------------
-- Has_Visible_Private_Ancestor --
-----------------------------------
function Has_Visible_Private_Ancestor (Id : E) return Boolean is
R : constant Entity_Id := Root_Type (Id);
T1 : Entity_Id := Id;
begin
loop
if Is_Private_Type (T1) then
return True;
elsif T1 = R then
return False;
else
T1 := Etype (T1);
end if;
end loop;
end Has_Visible_Private_Ancestor;
-------------------------
-- Top_Level_Aggregate --
......@@ -7101,7 +7112,7 @@ package body Exp_Aggr is
-- the back-end
else
Pass_Aggregate_To_Back_End;
Build_Back_End_Aggregate;
end if;
-- Gigi doesn't properly handle temporaries of variable size so we
......@@ -7178,7 +7189,7 @@ package body Exp_Aggr is
-- In all other cases, build a proper aggregate to be handled by gigi
else
Pass_Aggregate_To_Back_End;
Build_Back_End_Aggregate;
end if;
end Expand_Record_Aggregate;
......
......@@ -3286,9 +3286,12 @@ package body Exp_Ch4 is
-- very weird cases, so in the general case we need an overflow check on
-- the high bound. We can avoid this for the common case of string types
-- and other types whose index is Positive, since we chose a wider range
-- for the arithmetic type.
-- for the arithmetic type. If checks are suppressed we do not set the
-- flag, and possibly superfluous warnings will be omitted.
if Istyp /= Standard_Positive then
if Istyp /= Standard_Positive
and then not Overflow_Checks_Suppressed (Istyp)
then
Activate_Overflow_Check (High_Bound);
end if;
......
......@@ -420,7 +420,10 @@ begin
Instantiate_Bodies;
end if;
if Operating_Mode = Generate_Code then
-- Analyze inlined bodies and check elaboration rules in GNATprove
-- mode as well as during compilation.
if Operating_Mode = Generate_Code or else GNATprove_Mode then
if Inline_Processing_Required then
Analyze_Inlined_Bodies;
end if;
......
......@@ -701,10 +701,13 @@ package body SPARK_Specific is
end;
end loop;
for Index in Drefs.First .. Drefs.Last loop
Xrefs.Append (Drefs.Table (Index));
Nrefs := Nrefs + 1;
end loop;
declare
Drefs_Table : Drefs.Table_Type
renames Drefs.Table (Drefs.First .. Drefs.Last);
begin
Xrefs.Append_All (Xrefs.Table_Type (Drefs_Table));
Nrefs := Nrefs + Drefs_Table'Length;
end;
-- Capture the definition Sloc values. As in the case of normal cross
-- references, we have to wait until now to get the correct value.
......
......@@ -986,13 +986,16 @@ package body Sem_Aggr is
elsif Is_Array_Type (Typ) then
-- First a special test, for the case of a positional aggregate
-- of characters which can be replaced by a string literal.
-- First a special test, for the case of a positional aggregate of
-- characters which can be replaced by a string literal.
-- Do not perform this transformation if this was a string literal to
-- start with, whose components needed constraint checks, or if the
-- component type is non-static, because it will require those checks
-- and be transformed back into an aggregate.
-- Do not perform this transformation if this was a string literal
-- to start with, whose components needed constraint checks, or if
-- the component type is non-static, because it will require those
-- checks and be transformed back into an aggregate. If the index
-- type is not Integer the aggregate may represent a user-defined
-- string type but the context might need the original type so we
-- do not perform the transformation at this point.
if Number_Dimensions (Typ) = 1
and then Is_Standard_Character_Type (Component_Type (Typ))
......@@ -1002,6 +1005,8 @@ package body Sem_Aggr is
and then not Is_Bit_Packed_Array (Typ)
and then Nkind (Original_Node (Parent (N))) /= N_String_Literal
and then Is_OK_Static_Subtype (Component_Type (Typ))
and then Base_Type (Etype (First_Index (Typ))) =
Base_Type (Standard_Integer)
then
declare
Expr : Node_Id;
......
......@@ -33,6 +33,7 @@ with Einfo; use Einfo;
with Errout; use Errout;
with Eval_Fat; use Eval_Fat;
with Exp_Ch3; use Exp_Ch3;
with Exp_Ch7; use Exp_Ch7;
with Exp_Ch9; use Exp_Ch9;
with Exp_Disp; use Exp_Disp;
with Exp_Dist; use Exp_Dist;
......@@ -2153,6 +2154,17 @@ package body Sem_Ch3 is
-- (They have the sloc of the label as found in the source, and that
-- is ahead of the current declarative part).
procedure Build_Assertion_Bodies (Decls : List_Id; Context : Node_Id);
-- Create the subprogram bodies which verify the run-time semantics of
-- the pragmas listed below for each elibigle type found in declarative
-- list Decls. The pragmas are:
--
-- Default_Initial_Condition
-- Invariant
-- Type_Invariant
--
-- Context denotes the owner of the declarative list.
procedure Check_Entry_Contracts;
-- Perform a pre-analysis of the pre- and postconditions of an entry
-- declaration. This must be done before full resolution and creation
......@@ -2195,6 +2207,85 @@ package body Sem_Ch3 is
end loop;
end Adjust_Decl;
----------------------------
-- Build_Assertion_Bodies --
----------------------------
procedure Build_Assertion_Bodies (Decls : List_Id; Context : Node_Id) is
procedure Build_Assertion_Bodies_For_Type (Typ : Entity_Id);
-- Create the subprogram bodies which verify the run-time semantics
-- of the pragmas listed below for type Typ. The pragmas are:
--
-- Default_Initial_Condition
-- Invariant
-- Type_Invariant
-------------------------------------
-- Build_Assertion_Bodies_For_Type --
-------------------------------------
procedure Build_Assertion_Bodies_For_Type (Typ : Entity_Id) is
begin
-- Preanalyze and resolve the Default_Initial_Condition assertion
-- expression at the end of the declarations to catch any errors.
if Has_DIC (Typ) then
Build_DIC_Procedure_Body (Typ);
end if;
if Nkind (Context) = N_Package_Specification then
-- Preanalyze and resolve the invariants of a private type
-- at the end of the visible declarations to catch potential
-- errors. Inherited class-wide invariants are not included
-- because they have already been resolved.
if Decls = Visible_Declarations (Context)
and then Ekind_In (Typ, E_Limited_Private_Type,
E_Private_Type,
E_Record_Type_With_Private)
and then Has_Own_Invariants (Typ)
then
Build_Invariant_Procedure_Body
(Typ => Typ,
Partial_Invariant => True);
-- Preanalyze and resolve the invariants of a private type's
-- full view at the end of the private declarations to catch
-- potential errors.
elsif Decls = Private_Declarations (Context)
and then not Is_Private_Type (Typ)
and then Has_Private_Declaration (Typ)
and then Has_Invariants (Typ)
then
Build_Invariant_Procedure_Body (Typ);
end if;
end if;
end Build_Assertion_Bodies_For_Type;
-- Local variables
Decl : Node_Id;
Decl_Id : Entity_Id;
-- Start of processing for Build_Assertion_Bodies
begin
Decl := First (Decls);
while Present (Decl) loop
if Is_Declaration (Decl) then
Decl_Id := Defining_Entity (Decl);
if Is_Type (Decl_Id) then
Build_Assertion_Bodies_For_Type (Decl_Id);
end if;
end if;
Next (Decl);
end loop;
end Build_Assertion_Bodies;
---------------------------
-- Check_Entry_Contracts --
---------------------------
......@@ -2581,11 +2672,13 @@ package body Sem_Ch3 is
Decl := Next_Decl;
end loop;
-- Analyze the contracts of packages and their bodies
-- Post-freezing actions
if Present (L) then
Context := Parent (L);
-- Analyze the contracts of packages and their bodies
if Nkind (Context) = N_Package_Specification then
-- When a package has private declarations, its contract must be
......@@ -2643,6 +2736,15 @@ package body Sem_Ch3 is
-- protected, subprogram, or task body (SPARK RM 7.2.2(3)).
Check_State_Refinements (Context);
-- Create the subprogram bodies which verify the run-time semantics
-- of pragmas Default_Initial_Condition and [Type_]Invariant for all
-- types within the current declarative list. This ensures that all
-- assertion expressions are preanalyzed and resolved at the end of
-- the declarative part. Note that the resolution happens even when
-- freezing does not take place.
Build_Assertion_Bodies (L, Context);
end if;
end Analyze_Declarations;
......
......@@ -369,31 +369,29 @@ package body Sem_Ch6 is
Set_Is_Inlined (Prev);
Ret_Type := Etype (Prev);
-- An expression function that is a completion freezes the
-- expression. This means freezing the return type, and if it is an
-- access type, freezing its designated type as well.
-- An expression function which acts as a completion freezes the
-- expression. This means freezing the return type, and if it is
-- an access type, freezing its designated type as well.
-- Note that we cannot defer this freezing to the analysis of the
-- expression itself, because a freeze node might appear in a nested
-- scope, leading to an elaboration order issue in gigi.
-- An entity can only be frozen if it has a completion, so we must
-- check this explicitly. If it is declared elsewhere it will have
-- been frozen already, so only types declared in currently opened
-- scopes need to be tested.
Freeze_Before (N, Ret_Type);
if Ekind (Ret_Type) = E_Private_Type
and then In_Open_Scopes (Scope (Ret_Type))
-- An entity can only be frozen if it is complete, so if the type
-- is still unfrozen it must still be incomplete in some way, e.g.
-- a privte type without a full view, or a type derived from such
-- in an enclosing scope. Except in a generic context, such an
-- incomplete type is an error.
if not Is_Frozen (Ret_Type)
and then not Is_Generic_Type (Ret_Type)
and then not Is_Frozen (Ret_Type)
and then No (Full_View (Ret_Type))
and then not Inside_A_Generic
then
Error_Msg_NE
("premature use of private type&",
Result_Definition (Specification (N)), Ret_Type);
else
Freeze_Before (N, Ret_Type);
end if;
if Is_Access_Type (Etype (Prev)) then
......
......@@ -35,11 +35,9 @@ with Debug; use Debug;
with Einfo; use Einfo;
with Elists; use Elists;
with Errout; use Errout;
with Exp_Ch7; use Exp_Ch7;
with Exp_Disp; use Exp_Disp;
with Exp_Dist; use Exp_Dist;
with Exp_Dbug; use Exp_Dbug;
with Exp_Util; use Exp_Util;
with Freeze; use Freeze;
with Ghost; use Ghost;
with Lib; use Lib;
......@@ -1432,30 +1430,6 @@ package body Sem_Ch7 is
Error_Msg_N ("no declaration in visible part for incomplete}", E);
end if;
if Is_Type (E) then
-- Preanalyze and resolve the Default_Initial_Condition assertion
-- expression at the end of the visible declarations to catch any
-- errors.
if Has_DIC (E) then
Build_DIC_Procedure_Body (E);
end if;
-- Preanalyze and resolve the invariants of a private type at the
-- end of the visible declarations to catch potential errors. Note
-- that inherited class-wide invariants are not considered because
-- they have already been resolved.
if Ekind_In (E, E_Limited_Private_Type,
E_Private_Type,
E_Record_Type_With_Private)
and then Has_Own_Invariants (E)
then
Build_Invariant_Procedure_Body (E, Partial_Invariant => True);
end if;
end if;
Next_Entity (E);
end loop;
......@@ -1635,30 +1609,6 @@ package body Sem_Ch7 is
("full view of & does not have preelaborable initialization", E);
end if;
if Is_Type (E) and then Serious_Errors_Detected > 0 then
-- Preanalyze and resolve the Default_Initial_Condition assertion
-- expression at the end of the private declarations when freezing
-- did not take place due to errors or because the context is a
-- generic unit.
if Has_DIC (E) then
Build_DIC_Procedure_Body (E);
end if;
-- Preanalyze and resolve the invariants of a private type's full
-- view at the end of the private declarations in case freezing
-- did not take place either due to errors or because the context
-- is a generic unit.
if not Is_Private_Type (E)
and then Has_Private_Declaration (E)
and then Has_Invariants (E)
then
Build_Invariant_Procedure_Body (E);
end if;
end if;
Next_Entity (E);
end loop;
......
......@@ -932,13 +932,29 @@ package body Sem_Disp is
---------------------------------
procedure Check_Dispatching_Operation (Subp, Old_Subp : Entity_Id) is
Tagged_Type : Entity_Id;
Has_Dispatching_Parent : Boolean := False;
Body_Is_Last_Primitive : Boolean := False;
Has_Dispatching_Parent : Boolean := False;
Ovr_Subp : Entity_Id := Empty;
Tagged_Type : Entity_Id;
begin
if not Ekind_In (Subp, E_Procedure, E_Function) then
if not Ekind_In (Subp, E_Function, E_Procedure) then
return;
-- The Default_Initial_Condition procedure is not a primitive subprogram
-- even if it relates to a tagged type. This routine is not meant to be
-- inherited or overridden.
elsif Is_DIC_Procedure (Subp) then
return;
-- The "partial" and "full" type invariant procedures are not primitive
-- subprograms even if they relate to a tagged type. These routines are
-- not meant to be inherited or overridden.
elsif Is_Invariant_Procedure (Subp)
or else Is_Partial_Invariant_Procedure (Subp)
then
return;
end if;
......
......@@ -112,6 +112,9 @@ package body Sem_Elab is
-- The current scope of the call. This is restored when we complete the
-- delayed call, so that we do this in the right scope.
From_SPARK_Code : Boolean;
-- Save indication of whether this call is under SPARK_Mode => On
From_Elab_Code : Boolean;
-- Save indication of whether this call is from elaboration code
......@@ -1941,13 +1944,17 @@ package body Sem_Elab is
----------------------
procedure Check_Elab_Calls is
Save_SPARK_Mode : SPARK_Mode_Type;
begin
-- If expansion is disabled, do not generate any checks. Also skip
-- If expansion is disabled, do not generate any checks, unless we
-- are in GNATprove mode, so that errors are issued in GNATprove for
-- violations of static elaboration rules in SPARK code. Also skip
-- checks if any subunits are missing because in either case we lack the
-- full information that we need, and no object file will be created in
-- any case.
if not Expander_Active
if (not Expander_Active and not GNATprove_Mode)
or else Is_Generic_Unit (Cunit_Entity (Main_Unit))
or else Subunits_Missing
then
......@@ -1964,12 +1971,21 @@ package body Sem_Elab is
Push_Scope (Delay_Check.Table (J).Curscop);
From_Elab_Code := Delay_Check.Table (J).From_Elab_Code;
-- Set appropriate value of SPARK_Mode
Save_SPARK_Mode := SPARK_Mode;
if Delay_Check.Table (J).From_SPARK_Code then
SPARK_Mode := On;
end if;
Check_Internal_Call_Continue (
N => Delay_Check.Table (J).N,
E => Delay_Check.Table (J).E,
Outer_Scope => Delay_Check.Table (J).Outer_Scope,
Orig_Ent => Delay_Check.Table (J).Orig_Ent);
SPARK_Mode := Save_SPARK_Mode;
Pop_Scope;
end loop;
......@@ -2223,12 +2239,13 @@ package body Sem_Elab is
if Delaying_Elab_Checks then
Delay_Check.Append (
(N => N,
E => E,
Orig_Ent => Orig_Ent,
Curscop => Current_Scope,
Outer_Scope => Outer_Scope,
From_Elab_Code => From_Elab_Code));
(N => N,
E => E,
Orig_Ent => Orig_Ent,
Curscop => Current_Scope,
Outer_Scope => Outer_Scope,
From_Elab_Code => From_Elab_Code,
From_SPARK_Code => SPARK_Mode = On));
return;
-- Otherwise, call phase 2 continuation right now
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment