+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
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
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
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;
----------------------
-- 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
-- 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
-- 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.
-- 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;
-- 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.
---------------------------
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))));
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
-- 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
-- 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 :=
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));
if Present (Orig_Tag) then
Tag_Value := Orig_Tag;
+
elsif not Tagged_Type_Expansion then
Tag_Value := Empty;
+
else
Tag_Value :=
New_Occurrence_Of
-- 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
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 --
-- 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
-- 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;
-- 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;
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;
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.
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))
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;
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;
-- (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
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 --
---------------------------
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
-- 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;
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
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;
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;
("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;
---------------------------------
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;
-- 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
----------------------
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
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;
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
projects / platform / upstream / gcc.git / commitdiff