CbC/CbC_gcc: gcc/ada/sem_util.adb comparison

comparison gcc/ada/sem_util.adb @ 131:84e7813d76e9

gcc-8.2

author	mir3636
date	Thu, 25 Oct 2018 07:37:49 +0900
parents	04ced10e8804
children	1830386684a0

comparison

equal deleted inserted replaced

-:04ced10e8804
+:84e7813d76e9
 --                                                                          --
 --                             S E M _ U T I L                              --
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2017, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2018, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
 -- ware  Foundation;  either version 3,  or (at your option) any later ver- --
 -- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
 with Debug;    use Debug;
 with Elists;   use Elists;
 with Errout;   use Errout;
 with Erroutc;  use Erroutc;
 with Exp_Ch11; use Exp_Ch11;
-with Exp_Disp; use Exp_Disp;
 with Exp_Util; use Exp_Util;
 with Fname;    use Fname;
 with Freeze;   use Freeze;
 with Lib;      use Lib;
 with Lib.Xref; use Lib.Xref;
 with GNAT.HTable; use GNAT.HTable;
 package body Sem_Util is
+---------------------------
+-- Local Data Structures --
+---------------------------
+Invalid_Binder_Values : array (Scalar_Id) of Entity_Id := (others => Empty);
+--  A collection to hold the entities of the variables declared in package
+--  System.Scalar_Values which describe the invalid values of scalar types.
+Invalid_Binder_Values_Set : Boolean := False;
+--  This flag prevents multiple attempts to initialize Invalid_Binder_Values
+Invalid_Floats : array (Float_Scalar_Id) of Ureal := (others => No_Ureal);
+--  A collection to hold the invalid values of float types as specified by
+--  pragma Initialize_Scalars.
+Invalid_Integers : array (Integer_Scalar_Id) of Uint := (others => No_Uint);
+--  A collection to hold the invalid values of integer types as specified
+--  by pragma Initialize_Scalars.
 -----------------------
 -- Local Subprograms --
 -----------------------
 function Build_Component_Subtype
 Loc : Source_Ptr;
 T   : Entity_Id) return Node_Id;
 --  This function builds the subtype for Build_Actual_Subtype_Of_Component
 --  and Build_Discriminal_Subtype_Of_Component. C is a list of constraints,
 --  Loc is the source location, T is the original subtype.
+procedure Examine_Array_Bounds
+(Typ        : Entity_Id;
+All_Static : out Boolean;
+Has_Empty  : out Boolean);
+--  Inspect the index constraints of array type Typ. Flag All_Static is set
+--  when all ranges are static. Flag Has_Empty is set only when All_Static
+--  is set and indicates that at least one range is empty.
 function Has_Enabled_Property
 (Item_Id  : Entity_Id;
 Property : Name_Id) return Boolean;
 --  Subsidiary to routines Async_xxx_Enabled and Effective_xxx_Enabled.
 --  becomes Requires_Transient_Scope and Old_Requires_Transient_Scope is
 --  eliminated.
 function Subprogram_Name (N : Node_Id) return String;
 --  Return the fully qualified name of the enclosing subprogram for the
---  given node N.
+--  given node N, with file:line:col information appended, e.g.
+--  "subp:file:line:col", corresponding to the source location of the
+--  body of the subprogram.
 ------------------------------
 --  Abstract_Interface_List --
 ------------------------------
 if Is_Concurrent_Type (Typ) then
 --  If we are dealing with a synchronized subtype, go to the base
 --  type, whose declaration has the interface list.
---  Shouldn't this be Declaration_Node???
+Nod := Declaration_Node (Base_Type (Typ));
-Nod := Parent (Base_Type (Typ));
+if Nkind_In (Nod, N_Full_Type_Declaration,
+N_Private_Type_Declaration)
-if Nkind (Nod) = N_Full_Type_Declaration then
+then
 return Empty_List;
 end if;
 elsif Ekind (Typ) = E_Record_Type_With_Private then
 if Nkind (Parent (Typ)) = N_Full_Type_Declaration then
 -----------
 -- Inner --
 -----------
 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
 --  is needed for some cases of instantiations.
 Inner (Scope (E));
 return;
 end if;
 end;
+Scop := Scope (E);
 --  Just print entity name if its scope is at the outer level
-if Scope (E) = Standard_Standard then
+if Scop = Standard_Standard then
 null;
 --  If scope comes from source, write scope and entity
-elsif Comes_From_Source (Scope (E)) then
+elsif Comes_From_Source (Scop) then
-Append_Entity_Name (Temp, Scope (E));
+Append_Entity_Name (Temp, Scop);
 Append (Temp, '.');
 --  If in wrapper package skip past it
-elsif Is_Wrapper_Package (Scope (E)) then
+elsif Present (Scop) and then Is_Wrapper_Package (Scop) then
-Append_Entity_Name (Temp, Scope (Scope (E)));
+Append_Entity_Name (Temp, Scope (Scop));
 Append (Temp, '.');
 --  Otherwise nothing to output (happens in unnamed block statements)
 else
 and then Has_Private_Declaration (Typ)
 and then Is_Tagged_Type (Typ)
 and then Scop = Current_Scope
 then
 --  The inherited operation is available at the earliest place after
---  the derived type declaration ( RM 7.3.1 (6/1)). This is only
+--  the derived type declaration (RM 7.3.1 (6/1)). This is only
 --  relevant for type extensions. If the parent operation appears
 --  after the type extension, the operation is not visible.
 Decl := First
 (Visible_Declarations
 if Nkind (Decl) = N_Private_Extension_Declaration
 and then Defining_Entity (Decl) = Typ
 then
 if Sloc (Decl) > Sloc (Par) then
 Next_E := Next_Entity (Par);
-Set_Next_Entity (Par, S);
+Link_Entities (Par, S);
-Set_Next_Entity (S, Next_E);
+Link_Entities (S, Next_E);
 return;
 else
 exit;
 end if;
 --  The new operation is internal and overriding indicators do not apply
 --  (the original primitive may have carried one).
 Set_Must_Override (Specification (Clone_Body), False);
-Insert_Before (Bod, Clone_Body);
+--  If the subprogram body is the proper body of a stub, insert the
+--  subprogram after the stub, i.e. the same declarative region as
+--  the original sugprogram.
+if Nkind (Parent (Bod)) = N_Subunit then
+Insert_After (Corresponding_Stub (Parent (Bod)), Clone_Body);
+else
+Insert_Before (Bod, Clone_Body);
+end if;
 Analyze (Clone_Body);
 end Build_Class_Wide_Clone_Body;
 ---------------------------------
 -- Build_Class_Wide_Clone_Call --
 Scop        : Entity_Id;
 begin
 pragma Assert (Ekind_In (Id, E_Abstract_State, E_Variable));
+--  Nothing to do for internally-generated abstract states and variables
+--  because they do not represent the hidden state of the source unit.
+if not Comes_From_Source (Id) then
+return;
+end if;
 --  Find the proper context where the object or state appears
 Scop := Scope (Id);
 while Present (Scop) loop
 Context := Scop;
 -----------------------------
 -- Check_Part_Of_Reference --
 -----------------------------
 procedure Check_Part_Of_Reference (Var_Id : Entity_Id; Ref : Node_Id) is
+function Is_Enclosing_Package_Body
+(Body_Decl : Node_Id;
+Obj_Id    : Entity_Id) return Boolean;
+pragma Inline (Is_Enclosing_Package_Body);
+--  Determine whether package body Body_Decl or its corresponding spec
+--  immediately encloses the declaration of object Obj_Id.
+function Is_Internal_Declaration_Or_Body
+(Decl : Node_Id) return Boolean;
+pragma Inline (Is_Internal_Declaration_Or_Body);
+--  Determine whether declaration or body denoted by Decl is internal
+function Is_Single_Declaration_Or_Body
+(Decl     : Node_Id;
+Conc_Typ : Entity_Id) return Boolean;
+pragma Inline (Is_Single_Declaration_Or_Body);
+--  Determine whether protected/task declaration or body denoted by Decl
+--  belongs to single concurrent type Conc_Typ.
+function Is_Single_Task_Pragma
+(Prag     : Node_Id;
+Task_Typ : Entity_Id) return Boolean;
+pragma Inline (Is_Single_Task_Pragma);
+--  Determine whether pragma Prag belongs to single task type Task_Typ
+-------------------------------
+-- Is_Enclosing_Package_Body --
+-------------------------------
+function Is_Enclosing_Package_Body
+(Body_Decl : Node_Id;
+Obj_Id    : Entity_Id) return Boolean
+is
+Obj_Context : Node_Id;
+begin
+--  Find the context of the object declaration
+Obj_Context := Parent (Declaration_Node (Obj_Id));
+if Nkind (Obj_Context) = N_Package_Specification then
+Obj_Context := Parent (Obj_Context);
+end if;
+--  The object appears immediately within the package body
+if Obj_Context = Body_Decl then
+return True;
+--  The object appears immediately within the corresponding spec
+elsif Nkind (Obj_Context) = N_Package_Declaration
+and then Unit_Declaration_Node (Corresponding_Spec (Body_Decl)) =
+Obj_Context
+then
+return True;
+end if;
+return False;
+end Is_Enclosing_Package_Body;
+-------------------------------------
+-- Is_Internal_Declaration_Or_Body --
+-------------------------------------
+function Is_Internal_Declaration_Or_Body
+(Decl : Node_Id) return Boolean
+is
+begin
+if Comes_From_Source (Decl) then
+return False;
+--  A body generated for an expression function which has not been
+--  inserted into the tree yet (In_Spec_Expression is True) is not
+--  considered internal.
+elsif Nkind (Decl) = N_Subprogram_Body
+and then Was_Expression_Function (Decl)
+and then not In_Spec_Expression
+then
+return False;
+end if;
+return True;
+end Is_Internal_Declaration_Or_Body;
+-----------------------------------
+-- Is_Single_Declaration_Or_Body --
+-----------------------------------
+function Is_Single_Declaration_Or_Body
+(Decl     : Node_Id;
+Conc_Typ : Entity_Id) return Boolean
+is
+Spec_Id : constant Entity_Id := Unique_Defining_Entity (Decl);
+begin
+return
+Present (Anonymous_Object (Spec_Id))
+and then Anonymous_Object (Spec_Id) = Conc_Typ;
+end Is_Single_Declaration_Or_Body;
+---------------------------
+-- Is_Single_Task_Pragma --
+---------------------------
+function Is_Single_Task_Pragma
+(Prag     : Node_Id;
+Task_Typ : Entity_Id) return Boolean
+is
+Decl : constant Node_Id := Find_Related_Declaration_Or_Body (Prag);
+begin
+--  To qualify, the pragma must be associated with single task type
+--  Task_Typ.
+return
+Is_Single_Task_Object (Task_Typ)
+and then Nkind (Decl) = N_Object_Declaration
+and then Defining_Entity (Decl) = Task_Typ;
+end Is_Single_Task_Pragma;
+--  Local variables
 Conc_Obj : constant Entity_Id := Encapsulating_State (Var_Id);
-Decl     : Node_Id;
-OK_Use   : Boolean := False;
 Par      : Node_Id;
 Prag_Nam : Name_Id;
-Spec_Id  : Entity_Id;
+Prev     : Node_Id;
-begin
+--  Start of processing for Check_Part_Of_Reference
+begin
+--  Nothing to do when the variable was recorded, but did not become a
+--  constituent of a single concurrent type.
+if No (Conc_Obj) then
+return;
+end if;
 --  Traverse the parent chain looking for a suitable context for the
 --  reference to the concurrent constituent.
-Par := Parent (Ref);
+Prev := Ref;
+Par  := Parent (Prev);
 while Present (Par) loop
 if Nkind (Par) = N_Pragma then
 Prag_Nam := Pragma_Name (Par);
 --  A concurrent constituent is allowed to appear in pragmas
 --  Initial_Condition and Initializes as this is part of the
---  elaboration checks for the constituent (SPARK RM 9.3).
+--  elaboration checks for the constituent (SPARK RM 9(3)).
 if Nam_In (Prag_Nam, Name_Initial_Condition, Name_Initializes) then
-OK_Use := True;
+return;
-exit;
 --  When the reference appears within pragma Depends or Global,
 --  check whether the pragma applies to a single task type. Note
---  that the pragma is not encapsulated by the type definition,
+--  that the pragma may not encapsulated by the type definition,
 --  but this is still a valid context.
-elsif Nam_In (Prag_Nam, Name_Depends, Name_Global) then
+elsif Nam_In (Prag_Nam, Name_Depends, Name_Global)
-Decl := Find_Related_Declaration_Or_Body (Par);
+and then Is_Single_Task_Pragma (Par, Conc_Obj)
+then
-if Nkind (Decl) = N_Object_Declaration
+return;
-and then Defining_Entity (Decl) = Conc_Obj
-then
-OK_Use := True;
-exit;
-end if;
 end if;
---  The reference appears somewhere in the definition of the single
+--  The reference appears somewhere in the definition of a single
---  protected/task type (SPARK RM 9.3).
+--  concurrent type (SPARK RM 9(3)).
 elsif Nkind_In (Par, N_Single_Protected_Declaration,
 N_Single_Task_Declaration)
 and then Defining_Entity (Par) = Conc_Obj
 then
-OK_Use := True;
+return;
-exit;
+--  The reference appears within the declaration or body of a single
---  The reference appears within the expanded declaration or the body
+--  concurrent type (SPARK RM 9(3)).
---  of the single protected/task type (SPARK RM 9.3).
 elsif Nkind_In (Par, N_Protected_Body,
 N_Protected_Type_Declaration,
 N_Task_Body,
 N_Task_Type_Declaration)
+and then Is_Single_Declaration_Or_Body (Par, Conc_Obj)
 then
-Spec_Id := Unique_Defining_Entity (Par);
+return;
-if Present (Anonymous_Object (Spec_Id))
+--  The reference appears within the statement list of the object's
-and then Anonymous_Object (Spec_Id) = Conc_Obj
+--  immediately enclosing package (SPARK RM 9(3)).
-then
-OK_Use := True;
+elsif Nkind (Par) = N_Package_Body
-exit;
+and then Nkind (Prev) = N_Handled_Sequence_Of_Statements
-end if;
+and then Is_Enclosing_Package_Body (Par, Var_Id)
+then
+return;
 --  The reference has been relocated within an internally generated
 --  package or subprogram. Assume that the reference is legal as the
 --  real check was already performed in the original context of the
 --  reference.
 elsif Nkind_In (Par, N_Package_Body,
 N_Package_Declaration,
 N_Subprogram_Body,
 N_Subprogram_Declaration)
-and then not Comes_From_Source (Par)
+and then Is_Internal_Declaration_Or_Body (Par)
 then
---  Continue to examine the context if the reference appears in a
+return;
---  subprogram body which was previously an expression function,
---  unless this is during preanalysis (when In_Spec_Expression is
---  True), as the body may not yet be inserted in the tree.
-if Nkind (Par) = N_Subprogram_Body
-and then Was_Expression_Function (Par)
-and then not In_Spec_Expression
-then
-null;
---  Otherwise the reference is legal
-else
-OK_Use := True;
-exit;
-end if;
 --  The reference has been relocated to an inlined body for GNATprove.
 --  Assume that the reference is legal as the real check was already
 --  performed in the original context of the reference.
 elsif GNATprove_Mode
 and then Nkind (Par) = N_Subprogram_Body
 and then Chars (Defining_Entity (Par)) = Name_uParent
 then
-OK_Use := True;
+return;
-exit;
+end if;
-end if;
+Prev := Par;
-Par := Parent (Par);
+Par  := Parent (Prev);
 end loop;
---  The reference is illegal as it appears outside the definition or
+--  At this point it is known that the reference does not appear within a
---  body of the single protected/task type.
+--  legal context.
-if not OK_Use then
+Error_Msg_NE
+("reference to variable & cannot appear in this context", Ref, Var_Id);
+Error_Msg_Name_1 := Chars (Var_Id);
+if Is_Single_Protected_Object (Conc_Obj) then
 Error_Msg_NE
-("reference to variable & cannot appear in this context",
+("\% is constituent of single protected type &", Ref, Conc_Obj);
-Ref, Var_Id);
-Error_Msg_Name_1 := Chars (Var_Id);
+else
+Error_Msg_NE
-if Is_Single_Protected_Object (Conc_Obj) then
+("\% is constituent of single task type &", Ref, Conc_Obj);
-Error_Msg_NE
-("\% is constituent of single protected type &", Ref, Conc_Obj);
-else
-Error_Msg_NE
-("\% is constituent of single task type &", Ref, Conc_Obj);
-end if;
 end if;
 end Check_Part_Of_Reference;
 ------------------------------------------
 -- Check_Potentially_Blocking_Operation --
 begin
 if Is_Attribute_Result (N) then
 Result_Seen := True;
 return Abandon;
+--  Warn on infinite recursion if call is to current function
+elsif Nkind (N) = N_Function_Call
+and then Is_Entity_Name (Name (N))
+and then Entity (Name (N)) = Subp_Id
+and then not Is_Potentially_Unevaluated (N)
+then
+Error_Msg_NE
+("call to & within its postcondition will lead to infinite "
+& "recursion?", N, Subp_Id);
+return OK;
 --  Continue the traversal
 else
 return OK;
 end if;
 --  state refinement.
 if SPARK_Mode_Is_Off (Pack) then
 null;
---  State refinement can only occur in a completing packge body. Do
+--  State refinement can only occur in a completing package body. Do
 --  not verify proper state refinement when the body is subject to
 --  pragma SPARK_Mode Off because this disables the requirement for
 --  state refinement.
 elsif Present (Body_Id)
 ----------------------------------
 -- Collect_Primitive_Operations --
 ----------------------------------
 function Collect_Primitive_Operations (T : Entity_Id) return Elist_Id is
-B_Type         : constant Entity_Id := Base_Type (T);
+B_Type : constant Entity_Id := Base_Type (T);
-B_Decl         : constant Node_Id   := Original_Node (Parent (B_Type));
-B_Scope        : Entity_Id          := Scope (B_Type);
-Op_List        : Elist_Id;
-Formal         : Entity_Id;
-Is_Prim        : Boolean;
-Is_Type_In_Pkg : Boolean;
-Formal_Derived : Boolean := False;
-Id             : Entity_Id;
 function Match (E : Entity_Id) return Boolean;
 --  True if E's base type is B_Type, or E is of an anonymous access type
 --  and the base type of its designated type is B_Type.
 or else
 (Ada_Version >= Ada_2012
 and then Ekind (Etyp) = E_Incomplete_Type
 and then Full_View (Etyp) = B_Type);
 end Match;
+--  Local variables
+B_Decl         : constant Node_Id := Original_Node (Parent (B_Type));
+B_Scope        : Entity_Id        := Scope (B_Type);
+Op_List        : Elist_Id;
+Eq_Prims_List  : Elist_Id := No_Elist;
+Formal         : Entity_Id;
+Is_Prim        : Boolean;
+Is_Type_In_Pkg : Boolean;
+Formal_Derived : Boolean := False;
+Id             : Entity_Id;
 --  Start of processing for Collect_Primitive_Operations
 begin
 --  For tagged types, the primitive operations are collected as they
 end if;
 --  Locate the primitive subprograms of the type
 else
---  The primitive operations appear after the base type, except
+--  The primitive operations appear after the base type, except if the
---  if the derivation happens within the private part of B_Scope
+--  derivation happens within the private part of B_Scope and the type
---  and the type is a private type, in which case both the type
+--  is a private type, in which case both the type and some primitive
---  and some primitive operations may appear before the base
+--  operations may appear before the base type, and the list of
---  type, and the list of candidates starts after the type.
+--  candidates starts after the type.
 if In_Open_Scopes (B_Scope)
 and then Scope (T) = B_Scope
 and then In_Private_Part (B_Scope)
 then
 Id := Next_Entity (T);
---  In Ada 2012, If the type has an incomplete partial view, there
+--  In Ada 2012, If the type has an incomplete partial view, there may
---  may be primitive operations declared before the full view, so
+--  be primitive operations declared before the full view, so we need
---  we need to start scanning from the incomplete view, which is
+--  to start scanning from the incomplete view, which is earlier on
---  earlier on the entity chain.
+--  the entity chain.
 elsif Nkind (Parent (B_Type)) = N_Full_Type_Declaration
 and then Present (Incomplete_View (Parent (B_Type)))
 then
 Id := Defining_Entity (Incomplete_View (Parent (B_Type)));
 --  Include the subprogram in the list of primitives
 else
 Append_Elmt (Id, Op_List);
+--  Save collected equality primitives for later filtering
+--  (if we are processing a private type for which we can
+--  collect several candidates).
+if Inherits_From_Tagged_Full_View (T)
+and then Chars (Id) = Name_Op_Eq
+and then Etype (First_Formal (Id)) =
+Etype (Next_Formal (First_Formal (Id)))
+then
+if No (Eq_Prims_List) then
+Eq_Prims_List := New_Elmt_List;
+end if;
+Append_Elmt (Id, Eq_Prims_List);
+end if;
 end if;
 end if;
 end if;
 Next_Entity (Id);
 then
 B_Scope := System_Aux_Id;
 Id := First_Entity (System_Aux_Id);
 end if;
 end loop;
+--  Filter collected equality primitives
+if Inherits_From_Tagged_Full_View (T)
+and then Present (Eq_Prims_List)
+then
+declare
+First  : constant Elmt_Id := First_Elmt (Eq_Prims_List);
+Second : Elmt_Id;
+begin
+pragma Assert (No (Next_Elmt (First))
+or else No (Next_Elmt (Next_Elmt (First))));
+--  No action needed if we have collected a single equality
+--  primitive
+if Present (Next_Elmt (First)) then
+Second := Next_Elmt (First);
+if Is_Dispatching_Operation
+(Ultimate_Alias (Node (First)))
+then
+Remove (Op_List, Node (First));
+elsif Is_Dispatching_Operation
+(Ultimate_Alias (Node (Second)))
+then
+Remove (Op_List, Node (Second));
+else
+pragma Assert (False);
+raise Program_Error;
+end if;
+end if;
+end;
+end if;
 end if;
 return Op_List;
 end Collect_Primitive_Operations;
 begin
 if Has_Delayed_Freeze (Old_Ent) and then not Is_Frozen (Old_Ent) then
 Set_Has_Delayed_Freeze (New_Ent);
 end if;
 end Conditional_Delay;
-----------------------------
--- Contains_Refined_State --
-----------------------------
-function Contains_Refined_State (Prag : Node_Id) return Boolean is
-function Has_State_In_Dependency (List : Node_Id) return Boolean;
---  Determine whether a dependency list mentions a state with a visible
---  refinement.
-function Has_State_In_Global (List : Node_Id) return Boolean;
---  Determine whether a global list mentions a state with a visible
---  refinement.
-function Is_Refined_State (Item : Node_Id) return Boolean;
---  Determine whether Item is a reference to an abstract state with a
---  visible refinement.
------------------------------
--- Has_State_In_Dependency --
------------------------------
-function Has_State_In_Dependency (List : Node_Id) return Boolean is
-Clause : Node_Id;
-Output : Node_Id;
-begin
---  A null dependency list does not mention any states
-if Nkind (List) = N_Null then
-return False;
---  Dependency clauses appear as component associations of an
---  aggregate.
-elsif Nkind (List) = N_Aggregate
-and then Present (Component_Associations (List))
-then
-Clause := First (Component_Associations (List));
-while Present (Clause) loop
---  Inspect the outputs of a dependency clause
-Output := First (Choices (Clause));
-while Present (Output) loop
-if Is_Refined_State (Output) then
-return True;
-end if;
-Next (Output);
-end loop;
---  Inspect the outputs of a dependency clause
-if Is_Refined_State (Expression (Clause)) then
-return True;
-end if;
-Next (Clause);
-end loop;
---  If we get here, then none of the dependency clauses mention a
---  state with visible refinement.
-return False;
---  An illegal pragma managed to sneak in
-else
-raise Program_Error;
-end if;
-end Has_State_In_Dependency;
--------------------------
--- Has_State_In_Global --
--------------------------
-function Has_State_In_Global (List : Node_Id) return Boolean is
-Item : Node_Id;
-begin
---  A null global list does not mention any states
-if Nkind (List) = N_Null then
-return False;
---  Simple global list or moded global list declaration
-elsif Nkind (List) = N_Aggregate then
---  The declaration of a simple global list appear as a collection
---  of expressions.
-if Present (Expressions (List)) then
-Item := First (Expressions (List));
-while Present (Item) loop
-if Is_Refined_State (Item) then
-return True;
-end if;
-Next (Item);
-end loop;
---  The declaration of a moded global list appears as a collection
---  of component associations where individual choices denote
---  modes.
-else
-Item := First (Component_Associations (List));
-while Present (Item) loop
-if Has_State_In_Global (Expression (Item)) then
-return True;
-end if;
-Next (Item);
-end loop;
-end if;
---  If we get here, then the simple/moded global list did not
---  mention any states with a visible refinement.
-return False;
---  Single global item declaration
-elsif Is_Entity_Name (List) then
-return Is_Refined_State (List);
---  An illegal pragma managed to sneak in
-else
-raise Program_Error;
-end if;
-end Has_State_In_Global;
-----------------------
--- Is_Refined_State --
-----------------------
-function Is_Refined_State (Item : Node_Id) return Boolean is
-Elmt    : Node_Id;
-Item_Id : Entity_Id;
-begin
-if Nkind (Item) = N_Null then
-return False;
---  States cannot be subject to attribute 'Result. This case arises
---  in dependency relations.
-elsif Nkind (Item) = N_Attribute_Reference
-and then Attribute_Name (Item) = Name_Result
-then
-return False;
---  Multiple items appear as an aggregate. This case arises in
---  dependency relations.
-elsif Nkind (Item) = N_Aggregate
-and then Present (Expressions (Item))
-then
-Elmt := First (Expressions (Item));
-while Present (Elmt) loop
-if Is_Refined_State (Elmt) then
-return True;
-end if;
-Next (Elmt);
-end loop;
---  If we get here, then none of the inputs or outputs reference a
---  state with visible refinement.
-return False;
---  Single item
-else
-Item_Id := Entity_Of (Item);
-return
-Present (Item_Id)
-and then Ekind (Item_Id) = E_Abstract_State
-and then Has_Visible_Refinement (Item_Id);
-end if;
-end Is_Refined_State;
---  Local variables
-Arg : constant Node_Id :=
-Get_Pragma_Arg (First (Pragma_Argument_Associations (Prag)));
-Nam : constant Name_Id := Pragma_Name (Prag);
---  Start of processing for Contains_Refined_State
-begin
-if Nam = Name_Depends then
-return Has_State_In_Dependency (Arg);
-else pragma Assert (Nam = Name_Global);
-return Has_State_In_Global (Arg);
-end if;
-end Contains_Refined_State;
 -------------------------
 -- Copy_Component_List --
 -------------------------
 -------------------------
 -- Denotes_Same_Object --
 -------------------------
 function Denotes_Same_Object (A1, A2 : Node_Id) return Boolean is
-Obj1 : Node_Id := A1;
-Obj2 : Node_Id := A2;
-function Has_Prefix (N : Node_Id) return Boolean;
---  Return True if N has attribute Prefix
 function Is_Renaming (N : Node_Id) return Boolean;
 --  Return true if N names a renaming entity
 function Is_Valid_Renaming (N : Node_Id) return Boolean;
 --  For renamings, return False if the prefix of any dereference within
 --  the renamed object_name is a variable, or any expression within the
 --  renamed object_name contains references to variables or calls on
 --  nonstatic functions; otherwise return True (RM 6.4.1(6.10/3))
-----------------
--- Has_Prefix --
-----------------
-function Has_Prefix (N : Node_Id) return Boolean is
-begin
-return
-Nkind_In (N,
-N_Attribute_Reference,
-N_Expanded_Name,
-N_Explicit_Dereference,
-N_Indexed_Component,
-N_Reference,
-N_Selected_Component,
-N_Slice);
-end Has_Prefix;
 -----------------
 -- Is_Renaming --
 -----------------
 function Is_Renaming (N : Node_Id) return Boolean is
 begin
-return Is_Entity_Name (N)
+return
-and then Present (Renamed_Entity (Entity (N)));
+Is_Entity_Name (N) and then Present (Renamed_Entity (Entity (N)));
 end Is_Renaming;
 -----------------------
 -- Is_Valid_Renaming --
 -----------------------
 function Is_Valid_Renaming (N : Node_Id) return Boolean is
 function Check_Renaming (N : Node_Id) return Boolean;
 --  Recursive function used to traverse all the prefixes of N
+--------------------
+-- Check_Renaming --
+--------------------
 function Check_Renaming (N : Node_Id) return Boolean is
 begin
 if Is_Renaming (N)
 and then not Check_Renaming (Renamed_Entity (Entity (N)))
 --  Start of processing for Is_Valid_Renaming
 begin
 return Check_Renaming (N);
 end Is_Valid_Renaming;
+--  Local variables
+Obj1 : Node_Id := A1;
+Obj2 : Node_Id := A2;
 --  Start of processing for Denotes_Same_Object
 begin
 --  Both names statically denote the same stand-alone object or parameter
 begin
 while Present (Decl)
 and then not (Nkind (Decl) in N_Declaration
 or else
-Nkind (Decl) in N_Later_Decl_Item)
+Nkind (Decl) in N_Later_Decl_Item
+or else
+Nkind (Decl) = N_Number_Declaration)
 loop
 Decl := Parent (Decl);
 end loop;
 return Decl;
 --------------------------
 -- Enclosing_Subprogram --
 --------------------------
 function Enclosing_Subprogram (E : Entity_Id) return Entity_Id is
-Dynamic_Scope : constant Entity_Id := Enclosing_Dynamic_Scope (E);
+Dyn_Scop : constant Entity_Id := Enclosing_Dynamic_Scope (E);
 begin
-if Dynamic_Scope = Standard_Standard then
+if Dyn_Scop = Standard_Standard then
 return Empty;
-elsif Dynamic_Scope = Empty then
+elsif Dyn_Scop = Empty then
 return Empty;
-elsif Ekind (Dynamic_Scope) = E_Subprogram_Body then
+elsif Ekind (Dyn_Scop) = E_Subprogram_Body then
-return Corresponding_Spec (Parent (Parent (Dynamic_Scope)));
+return Corresponding_Spec (Parent (Parent (Dyn_Scop)));
-elsif Ekind (Dynamic_Scope) = E_Block
+elsif Ekind_In (Dyn_Scop, E_Block, E_Return_Statement) then
-or else Ekind (Dynamic_Scope) = E_Return_Statement
+return Enclosing_Subprogram (Dyn_Scop);
+elsif Ekind (Dyn_Scop) = E_Entry then
+--  For a task entry, return the enclosing subprogram of the
+--  task itself.
+if Ekind (Scope (Dyn_Scop)) = E_Task_Type then
+return Enclosing_Subprogram (Dyn_Scop);
+--  A protected entry is rewritten as a protected procedure which is
+--  the desired enclosing subprogram. This is relevant when unnesting
+--  a procedure local to an entry body.
+else
+return Protected_Body_Subprogram (Dyn_Scop);
+end if;
+elsif Ekind (Dyn_Scop) = E_Task_Type then
+return Get_Task_Body_Procedure (Dyn_Scop);
+--  The scope may appear as a private type or as a private extension
+--  whose completion is a task or protected type.
+elsif Ekind_In (Dyn_Scop, E_Limited_Private_Type,
+E_Record_Type_With_Private)
+and then Present (Full_View (Dyn_Scop))
+and then Ekind_In (Full_View (Dyn_Scop), E_Task_Type, E_Protected_Type)
 then
-return Enclosing_Subprogram (Dynamic_Scope);
+return Get_Task_Body_Procedure (Full_View (Dyn_Scop));
-elsif Ekind (Dynamic_Scope) = E_Task_Type then
+--  No body is generated if the protected operation is eliminated
-return Get_Task_Body_Procedure (Dynamic_Scope);
+elsif Convention (Dyn_Scop) = Convention_Protected
-elsif Ekind (Dynamic_Scope) = E_Limited_Private_Type
+and then not Is_Eliminated (Dyn_Scop)
-and then Present (Full_View (Dynamic_Scope))
+and then Present (Protected_Body_Subprogram (Dyn_Scop))
-and then Ekind (Full_View (Dynamic_Scope)) = E_Task_Type
 then
-return Get_Task_Body_Procedure (Full_View (Dynamic_Scope));
+return Protected_Body_Subprogram (Dyn_Scop);
---  No body is generated if the protected operation is eliminated
-elsif Convention (Dynamic_Scope) = Convention_Protected
-and then not Is_Eliminated (Dynamic_Scope)
-and then Present (Protected_Body_Subprogram (Dynamic_Scope))
-then
-return Protected_Body_Subprogram (Dynamic_Scope);
 else
-return Dynamic_Scope;
+return Dyn_Scop;
 end if;
 end Enclosing_Subprogram;
 --------------------------
 -- End_Keyword_Location --
 pragma Assert
 (Nkind (Parent (Decl)) = N_Generic_Subprogram_Declaration);
 null;
 else
-Set_Next_Entity (Prev, Next_Entity (E));
+Link_Entities (Prev, Next_Entity (E));
 if No (Next_Entity (Prev)) then
 Set_Last_Entity (Current_Scope, Prev);
 end if;
 --    Obj : ...;
 --    Ren : ... renames Obj;
 if Is_Entity_Name (Ren) then
-Id := Entity (Ren);
+--  Do not follow a renaming that goes through a generic formal,
+--  because these entities are hidden and must not be referenced
+--  from outside the generic.
+if Is_Hidden (Entity (Ren)) then
+exit;
+else
+Id := Entity (Ren);
+end if;
 --  The reference renames a function result. Check the original
 --  node in case expansion relocates the function call.
 --    Ren : ... renames Func_Call;
 end loop;
 end if;
 return Id;
 end Entity_Of;
+--------------------------
+-- Examine_Array_Bounds --
+--------------------------
+procedure Examine_Array_Bounds
+(Typ        : Entity_Id;
+All_Static : out Boolean;
+Has_Empty  : out Boolean)
+is
+function Is_OK_Static_Bound (Bound : Node_Id) return Boolean;
+--  Determine whether bound Bound is a suitable static bound
+------------------------
+-- Is_OK_Static_Bound --
+------------------------
+function Is_OK_Static_Bound (Bound : Node_Id) return Boolean is
+begin
+return
+not Error_Posted (Bound)
+and then Is_OK_Static_Expression (Bound);
+end Is_OK_Static_Bound;
+--  Local variables
+Hi_Bound : Node_Id;
+Index    : Node_Id;
+Lo_Bound : Node_Id;
+--  Start of processing for Examine_Array_Bounds
+begin
+--  An unconstrained array type does not have static bounds, and it is
+--  not known whether they are empty or not.
+if not Is_Constrained (Typ) then
+All_Static := False;
+Has_Empty  := False;
+--  A string literal has static bounds, and is not empty as long as it
+--  contains at least one character.
+elsif Ekind (Typ) = E_String_Literal_Subtype then
+All_Static := True;
+Has_Empty  := String_Literal_Length (Typ) > 0;
+end if;
+--  Assume that all bounds are static and not empty
+All_Static := True;
+Has_Empty  := False;
+--  Examine each index
+Index := First_Index (Typ);
+while Present (Index) loop
+if Is_Discrete_Type (Etype (Index)) then
+Get_Index_Bounds (Index, Lo_Bound, Hi_Bound);
+if Is_OK_Static_Bound (Lo_Bound)
+and then
+Is_OK_Static_Bound (Hi_Bound)
+then
+--  The static bounds produce an empty range
+if Is_Null_Range (Lo_Bound, Hi_Bound) then
+Has_Empty := True;
+end if;
+--  Otherwise at least one of the bounds is not static
+else
+All_Static := False;
+end if;
+--  Otherwise the index is non-discrete, therefore not static
+else
+All_Static := False;
+end if;
+Next_Index (Index);
+end loop;
+end Examine_Array_Bounds;
 --------------------------
 -- Explain_Limited_Type --
 --------------------------
 --  Should always find it
 raise Program_Error;
 end Find_Corresponding_Discriminant;
+-------------------
+-- Find_DIC_Type --
+-------------------
+function Find_DIC_Type (Typ : Entity_Id) return Entity_Id is
+Curr_Typ : Entity_Id;
+--  The current type being examined in the parent hierarchy traversal
+DIC_Typ : Entity_Id;
+--  The type which carries the DIC pragma. This variable denotes the
+--  partial view when private types are involved.
+Par_Typ : Entity_Id;
+--  The parent type of the current type. This variable denotes the full
+--  view when private types are involved.
+begin
+--  The input type defines its own DIC pragma, therefore it is the owner
+if Has_Own_DIC (Typ) then
+DIC_Typ := Typ;
+--  Otherwise the DIC pragma is inherited from a parent type
+else
+pragma Assert (Has_Inherited_DIC (Typ));
+--  Climb the parent chain
+Curr_Typ := Typ;
+loop
+--  Inspect the parent type. Do not consider subtypes as they
+--  inherit the DIC attributes from their base types.
+DIC_Typ := Base_Type (Etype (Curr_Typ));
+--  Look at the full view of a private type because the type may
+--  have a hidden parent introduced in the full view.
+Par_Typ := DIC_Typ;
+if Is_Private_Type (Par_Typ)
+and then Present (Full_View (Par_Typ))
+then
+Par_Typ := Full_View (Par_Typ);
+end if;
+--  Stop the climb once the nearest parent type which defines a DIC
+--  pragma of its own is encountered or when the root of the parent
+--  chain is reached.
+exit when Has_Own_DIC (DIC_Typ) or else Curr_Typ = Par_Typ;
+Curr_Typ := Par_Typ;
+end loop;
+end if;
+return DIC_Typ;
+end Find_DIC_Type;
 ----------------------------------
 -- Find_Enclosing_Iterator_Loop --
 ----------------------------------
 function Find_Enclosing_Iterator_Loop (Id : Entity_Id) return Entity_Id is
 --------------------------
 -- Find_Enclosing_Scope --
 --------------------------
 function Find_Enclosing_Scope (N : Node_Id) return Entity_Id is
-Par     : Node_Id;
+Par : Node_Id;
-Spec_Id : Entity_Id;
 begin
 --  Examine the parent chain looking for a construct which defines a
 --  scope.
 | N_Task_Type_Declaration
 =>
 return Defining_Entity (Par);
 --  The construct denotes a body, the proper scope is the entity of
---  the corresponding spec.
+--  the corresponding spec or that of the body if the body does not
+--  complete a previous declaration.
 when N_Entry_Body
 | N_Package_Body
 | N_Protected_Body
 | N_Subprogram_Body
 | N_Task_Body
 =>
-Spec_Id := Corresponding_Spec (Par);
+return Unique_Defining_Entity (Par);
---  The defining entity of a stand-alone subprogram body defines
---  a scope.
-if Nkind (Par) = N_Subprogram_Body and then No (Spec_Id) then
-return Defining_Entity (Par);
---  Otherwise there should be corresponding spec which defines a
---  scope.
-else
-pragma Assert (Present (Spec_Id));
-return Spec_Id;
-end if;
 --  Special cases
 --  Blocks carry either a source or an internally-generated scope,
 --  unless the block is a byproduct of exception handling.
 end if;
 Context := Scope (Context);
 end loop;
 end Find_Placement_In_State_Space;
+-----------------------
+-- Find_Primitive_Eq --
+-----------------------
+function Find_Primitive_Eq (Typ : Entity_Id) return Entity_Id is
+function Find_Eq_Prim (Prims_List : Elist_Id) return Entity_Id;
+--  Search for the equality primitive; return Empty if the primitive is
+--  not found.
+------------------
+-- Find_Eq_Prim --
+------------------
+function Find_Eq_Prim (Prims_List : Elist_Id) return Entity_Id is
+Prim      : Entity_Id;
+Prim_Elmt : Elmt_Id;
+begin
+Prim_Elmt := First_Elmt (Prims_List);
+while Present (Prim_Elmt) loop
+Prim := Node (Prim_Elmt);
+--  Locate primitive equality with the right signature
+if Chars (Prim) = Name_Op_Eq
+and then Etype (First_Formal (Prim)) =
+Etype (Next_Formal (First_Formal (Prim)))
+and then Base_Type (Etype (Prim)) = Standard_Boolean
+then
+return Prim;
+end if;
+Next_Elmt (Prim_Elmt);
+end loop;
+return Empty;
+end Find_Eq_Prim;
+--  Local Variables
+Eq_Prim   : Entity_Id;
+Full_Type : Entity_Id;
+--  Start of processing for Find_Primitive_Eq
+begin
+if Is_Private_Type (Typ) then
+Full_Type := Underlying_Type (Typ);
+else
+Full_Type := Typ;
+end if;
+if No (Full_Type) then
+return Empty;
+end if;
+Full_Type := Base_Type (Full_Type);
+--  When the base type itself is private, use the full view
+if Is_Private_Type (Full_Type) then
+Full_Type := Underlying_Type (Full_Type);
+end if;
+if Is_Class_Wide_Type (Full_Type) then
+Full_Type := Root_Type (Full_Type);
+end if;
+if not Is_Tagged_Type (Full_Type) then
+Eq_Prim := Find_Eq_Prim (Collect_Primitive_Operations (Typ));
+--  If this is an untagged private type completed with a derivation of
+--  an untagged private type whose full view is a tagged type, we use
+--  the primitive operations of the private parent type (since it does
+--  not have a full view, and also because its equality primitive may
+--  have been overridden in its untagged full view). If no equality was
+--  defined for it then take its dispatching equality primitive.
+elsif Inherits_From_Tagged_Full_View (Typ) then
+Eq_Prim := Find_Eq_Prim (Collect_Primitive_Operations (Typ));
+if No (Eq_Prim) then
+Eq_Prim := Find_Eq_Prim (Primitive_Operations (Full_Type));
+end if;
+else
+Eq_Prim := Find_Eq_Prim (Primitive_Operations (Full_Type));
+end if;
+return Eq_Prim;
+end Find_Primitive_Eq;
 ------------------------
 -- Find_Specific_Type --
 ------------------------
 --  The discriminant *must* be in the Governed_By List
 Assoc := First (Governed_By);
 Find_Constraint : loop
 Discrim := First (Choices (Assoc));
-exit Find_Constraint when Chars (Discrim_Name) = Chars (Discrim)
+exit Find_Constraint when
-or else (Present (Corresponding_Discriminant (Entity (Discrim)))
+Chars (Discrim_Name) = Chars (Discrim)
-and then
+or else
-Chars (Corresponding_Discriminant (Entity (Discrim))) =
+(Present (Corresponding_Discriminant (Entity (Discrim)))
-Chars  (Discrim_Name))
+and then Chars (Corresponding_Discriminant
-or else Chars (Original_Record_Component (Entity (Discrim)))
+(Entity (Discrim))) = Chars  (Discrim_Name))
-= Chars (Discrim_Name);
+or else
+Chars (Original_Record_Component (Entity (Discrim))) =
+Chars (Discrim_Name);
 if No (Next (Assoc)) then
-if not Is_Constrained (Typ)
+if not Is_Constrained (Typ) and then Is_Derived_Type (Typ) then
-and then Is_Derived_Type (Typ)
-and then Present (Stored_Constraint (Typ))
-then
 --  If the type is a tagged type with inherited discriminants,
 --  use the stored constraint on the parent in order to find
 --  the values of discriminants that are otherwise hidden by an
 --  explicit constraint. Renamed discriminants are handled in
 --  the code above.
 --  discriminant of the derived type, the call to obtain the
 --  Corresponding_Discriminant field only retrieves the last
 --  of them. We recover the constraint on the others from the
 --  Stored_Constraint as well.
+--  An inherited discriminant may have been constrained in a
+--  later ancestor (not the immediate parent) so we must examine
+--  the stored constraint of all of them to locate the inherited
+--  value.
 declare
+C : Elmt_Id;
 D : Entity_Id;
-C : Elmt_Id;
+T : Entity_Id := Typ;
 begin
-D := First_Discriminant (Etype (Typ));
+while Is_Derived_Type (T) loop
-C := First_Elmt (Stored_Constraint (Typ));
+if Present (Stored_Constraint (T)) then
-while Present (D) and then Present (C) loop
+D := First_Discriminant (Etype (T));
-if Chars (Discrim_Name) = Chars (D) then
+C := First_Elmt (Stored_Constraint (T));
-if Is_Entity_Name (Node (C))
+while Present (D) and then Present (C) loop
-and then Entity (Node (C)) = Entity (Discrim)
+if Chars (Discrim_Name) = Chars (D) then
-then
+if Is_Entity_Name (Node (C))
---  D is renamed by Discrim, whose value is given in
+and then Entity (Node (C)) = Entity (Discrim)
---  Assoc.
+then
+--  D is renamed by Discrim, whose value is
-null;
+--  given in Assoc.
-else
+null;
-Assoc :=
-Make_Component_Association (Sloc (Typ),
+else
-New_List
+Assoc :=
-(New_Occurrence_Of (D, Sloc (Typ))),
+Make_Component_Association (Sloc (Typ),
-Duplicate_Subexpr_No_Checks (Node (C)));
+New_List
-end if;
+(New_Occurrence_Of (D, Sloc (Typ))),
-exit Find_Constraint;
+Duplicate_Subexpr_No_Checks (Node (C)));
+end if;
+exit Find_Constraint;
+end if;
+Next_Discriminant (D);
+Next_Elmt (C);
+end loop;
 end if;
-Next_Discriminant (D);
+--  Discriminant may be inherited from ancestor
-Next_Elmt (C);
+T := Etype (T);
 end loop;
 end;
 end if;
 end if;
 if No (Next (Assoc)) then
-Error_Msg_NE (" missing value for discriminant&",
+Error_Msg_NE
-First (Governed_By), Discrim_Name);
+(" missing value for discriminant&",
+First (Governed_By), Discrim_Name);
 Report_Errors := True;
 return;
 end if;
 Next (Assoc);
 if Is_Private_Type (Btyp) and then Present (Full_View (Btyp)) then
 Btyp := Full_View (Btyp);
 end if;
 Lit := First_Literal (Btyp);
+--  Position in the enumeration type starts at 0
+if UI_To_Int (Pos) < 0 then
+raise Constraint_Error;
+end if;
 for J in 1 .. UI_To_Int (Pos) loop
 Next_Literal (Lit);
 --  If Lit is Empty, Pos is not in range, so raise Constraint_Error
 --  inside the loop to avoid calling Next_Literal on Empty.
 return Empty;
 end if;
 end Get_Iterable_Type_Primitive;
 ----------------------------------
--- Get_Library_Unit_Name_string --
+-- Get_Library_Unit_Name_String --
 ----------------------------------
 procedure Get_Library_Unit_Name_String (Decl_Node : Node_Id) is
 Unit_Name_Id : constant Unit_Name_Type := Get_Unit_Name (Decl_Node);
 --------------------------------
 -- State_Has_Enabled_Property --
 --------------------------------
 function State_Has_Enabled_Property return Boolean is
-Decl     : constant Node_Id := Parent (Item_Id);
+Decl : constant Node_Id := Parent (Item_Id);
-Opt      : Node_Id;
-Opt_Nam  : Node_Id;
+procedure Find_Simple_Properties
-Prop     : Node_Id;
+(Has_External    : out Boolean;
-Prop_Nam : Node_Id;
+Has_Synchronous : out Boolean);
-Props    : Node_Id;
+--  Extract the simple properties associated with declaration Decl
+function Is_Enabled_External_Property return Boolean;
+--  Determine whether property Property appears within the external
+--  property list of declaration Decl, and return its status.
+----------------------------
+-- Find_Simple_Properties --
+----------------------------
+procedure Find_Simple_Properties
+(Has_External    : out Boolean;
+Has_Synchronous : out Boolean)
+is
+Opt : Node_Id;
+begin
+--  Assume that none of the properties are available
+Has_External    := False;
+Has_Synchronous := False;
+Opt := First (Expressions (Decl));
+while Present (Opt) loop
+if Nkind (Opt) = N_Identifier then
+if Chars (Opt) = Name_External then
+Has_External := True;
+elsif Chars (Opt) = Name_Synchronous then
+Has_Synchronous := True;
+end if;
+end if;
+Next (Opt);
+end loop;
+end Find_Simple_Properties;
+----------------------------------
+-- Is_Enabled_External_Property --
+----------------------------------
+function Is_Enabled_External_Property return Boolean is
+Opt      : Node_Id;
+Opt_Nam  : Node_Id;
+Prop     : Node_Id;
+Prop_Nam : Node_Id;
+Props    : Node_Id;
+begin
+Opt := First (Component_Associations (Decl));
+while Present (Opt) loop
+Opt_Nam := First (Choices (Opt));
+if Nkind (Opt_Nam) = N_Identifier
+and then Chars (Opt_Nam) = Name_External
+then
+Props := Expression (Opt);
+--  Multiple properties appear as an aggregate
+if Nkind (Props) = N_Aggregate then
+--  Simple property form
+Prop := First (Expressions (Props));
+while Present (Prop) loop
+if Chars (Prop) = Property then
+return True;
+end if;
+Next (Prop);
+end loop;
+--  Property with expression form
+Prop := First (Component_Associations (Props));
+while Present (Prop) loop
+Prop_Nam := First (Choices (Prop));
+--  The property can be represented in two ways:
+--      others   => <value>
+--    <property> => <value>
+if Nkind (Prop_Nam) = N_Others_Choice
+or else (Nkind (Prop_Nam) = N_Identifier
+and then Chars (Prop_Nam) = Property)
+then
+return Is_True (Expr_Value (Expression (Prop)));
+end if;
+Next (Prop);
+end loop;
+--  Single property
+else
+return Chars (Props) = Property;
+end if;
+end if;
+Next (Opt);
+end loop;
+return False;
+end Is_Enabled_External_Property;
+--  Local variables
+Has_External    : Boolean;
+Has_Synchronous : Boolean;
+--  Start of processing for State_Has_Enabled_Property
 begin
 --  The declaration of an external abstract state appears as an
---  extension aggregate. If this is not the case, properties can never
+--  extension aggregate. If this is not the case, properties can
---  be set.
+--  never be set.
 if Nkind (Decl) /= N_Extension_Aggregate then
 return False;
 end if;
---  When External appears as a simple option, it automatically enables
+Find_Simple_Properties (Has_External, Has_Synchronous);
---  all properties.
+--  Simple option External enables all properties (SPARK RM 7.1.2(2))
-Opt := First (Expressions (Decl));
-while Present (Opt) loop
+if Has_External then
-if Nkind (Opt) = N_Identifier
+return True;
-and then Chars (Opt) = Name_External
-then
+--  Option External may enable or disable specific properties
-return True;
-end if;
+elsif Is_Enabled_External_Property then
+return True;
-Next (Opt);
-end loop;
+--  Simple option Synchronous
+--
---  When External specifies particular properties, inspect those and
+--    enables                disables
---  find the desired one (if any).
+--       Asynch_Readers         Effective_Reads
+--       Asynch_Writers         Effective_Writes
-Opt := First (Component_Associations (Decl));
+--
-while Present (Opt) loop
+--  Note that both forms of External have higher precedence than
-Opt_Nam := First (Choices (Opt));
+--  Synchronous (SPARK RM 7.1.4(10)).
-if Nkind (Opt_Nam) = N_Identifier
+elsif Has_Synchronous then
-and then Chars (Opt_Nam) = Name_External
+return Nam_In (Property, Name_Async_Readers, Name_Async_Writers);
-then
+end if;
-Props := Expression (Opt);
---  Multiple properties appear as an aggregate
-if Nkind (Props) = N_Aggregate then
---  Simple property form
-Prop := First (Expressions (Props));
-while Present (Prop) loop
-if Chars (Prop) = Property then
-return True;
-end if;
-Next (Prop);
-end loop;
---  Property with expression form
-Prop := First (Component_Associations (Props));
-while Present (Prop) loop
-Prop_Nam := First (Choices (Prop));
---  The property can be represented in two ways:
---      others   => <value>
---    <property> => <value>
-if Nkind (Prop_Nam) = N_Others_Choice
-or else (Nkind (Prop_Nam) = N_Identifier
-and then Chars (Prop_Nam) = Property)
-then
-return Is_True (Expr_Value (Expression (Prop)));
-end if;
-Next (Prop);
-end loop;
---  Single property
-else
-return Chars (Props) = Property;
-end if;
-end if;
-Next (Opt);
-end loop;
 return False;
 end State_Has_Enabled_Property;
 -----------------------------------
 -- Has_Full_Default_Initialization --
 -------------------------------------
 function Has_Full_Default_Initialization (Typ : Entity_Id) return Boolean is
 Comp : Entity_Id;
-Prag : Node_Id;
+begin
-begin
+--  A type subject to pragma Default_Initial_Condition may be fully
---  A type subject to pragma Default_Initial_Condition is fully default
+--  default initialized depending on inheritance and the argument of
---  initialized when the pragma appears with a non-null argument. Since
+--  the pragma. Since any type may act as the full view of a private
---  any type may act as the full view of a private type, this check must
+--  type, this check must be performed prior to the specialized tests
---  be performed prior to the specialized tests below.
+--  below.
-if Has_DIC (Typ) then
+if Has_Fully_Default_Initializing_DIC_Pragma (Typ) then
-Prag := Get_Pragma (Typ, Pragma_Default_Initial_Condition);
+return True;
-pragma Assert (Present (Prag));
-return Is_Verifiable_DIC_Pragma (Prag);
 end if;
 --  A scalar type is fully default initialized if it is subject to aspect
 --  Default_Value.
 else
 return False;
 end if;
 end Has_Full_Default_Initialization;
+-----------------------------------------------
+-- Has_Fully_Default_Initializing_DIC_Pragma --
+-----------------------------------------------
+function Has_Fully_Default_Initializing_DIC_Pragma
+(Typ : Entity_Id) return Boolean
+is
+Args : List_Id;
+Prag : Node_Id;
+begin
+--  A type that inherits pragma Default_Initial_Condition from a parent
+--  type is automatically fully default initialized.
+if Has_Inherited_DIC (Typ) then
+return True;
+--  Otherwise the type is fully default initialized only when the pragma
+--  appears without an argument, or the argument is non-null.
+elsif Has_Own_DIC (Typ) then
+Prag := Get_Pragma (Typ, Pragma_Default_Initial_Condition);
+pragma Assert (Present (Prag));
+Args := Pragma_Argument_Associations (Prag);
+--  The pragma appears without an argument in which case it defaults
+--  to True.
+if No (Args) then
+return True;
+--  The pragma appears with a non-null expression
+elsif Nkind (Get_Pragma_Arg (First (Args))) /= N_Null then
+return True;
+end if;
+end if;
+return False;
+end Has_Fully_Default_Initializing_DIC_Pragma;
 --------------------
 -- Has_Infinities --
 --------------------
 function Has_Infinities (E : Entity_Id) return Boolean is
 return
 Present (Constits)
 and then Nkind (Node (First_Elmt (Constits))) /= N_Null;
 end Has_Non_Null_Refinement;
+-----------------------------
+-- Has_Non_Null_Statements --
+-----------------------------
+function Has_Non_Null_Statements (L : List_Id) return Boolean is
+Node : Node_Id;
+begin
+if Is_Non_Empty_List (L) then
+Node := First (L);
+loop
+if Nkind (Node) /= N_Null_Statement then
+return True;
+end if;
+Next (Node);
+exit when Node = Empty;
+end loop;
+end if;
+return False;
+end Has_Non_Null_Statements;
 ----------------------------------
 -- Has_Non_Trivial_Precondition --
 ----------------------------------
 end if;
 return Has_PE;
 end Has_Preelaborable_Initialization;
+----------------
+-- Has_Prefix --
+----------------
+function Has_Prefix (N : Node_Id) return Boolean is
+begin
+return
+Nkind_In (N, N_Attribute_Reference,
+N_Expanded_Name,
+N_Explicit_Dereference,
+N_Indexed_Component,
+N_Reference,
+N_Selected_Component,
+N_Slice);
+end Has_Prefix;
 ---------------------------
 -- Has_Private_Component --
 ---------------------------
 function Has_Private_Component (Type_Id : Entity_Id) return Boolean is
 -----------------------------
 -- Has_Static_Array_Bounds --
 -----------------------------
 function Has_Static_Array_Bounds (Typ : Node_Id) return Boolean is
-Ndims : constant Nat := Number_Dimensions (Typ);
+All_Static : Boolean;
+Dummy      : Boolean;
-Index : Node_Id;
-Low   : Node_Id;
+begin
-High  : Node_Id;
+Examine_Array_Bounds (Typ, All_Static, Dummy);
-begin
+return All_Static;
---  Unconstrained types do not have static bounds
-if not Is_Constrained (Typ) then
-return False;
-end if;
---  First treat string literals specially, as the lower bound and length
---  of string literals are not stored like those of arrays.
---  A string literal always has static bounds
-if Ekind (Typ) = E_String_Literal_Subtype then
-return True;
-end if;
---  Treat all dimensions in turn
-Index := First_Index (Typ);
-for Indx in 1 .. Ndims loop
---  In case of an illegal index which is not a discrete type, return
---  that the type is not static.
-if not Is_Discrete_Type (Etype (Index))
-or else Etype (Index) = Any_Type
-then
-return False;
-end if;
-Get_Index_Bounds (Index, Low, High);
-if Error_Posted (Low) or else Error_Posted (High) then
-return False;
-end if;
-if Is_OK_Static_Expression (Low)
-and then
-Is_OK_Static_Expression (High)
-then
-null;
-else
-return False;
-end if;
-Next (Index);
-end loop;
---  If we fall through the loop, all indexes matched
-return True;
 end Has_Static_Array_Bounds;
+---------------------------------------
+-- Has_Static_Non_Empty_Array_Bounds --
+---------------------------------------
+function Has_Static_Non_Empty_Array_Bounds (Typ : Node_Id) return Boolean is
+All_Static : Boolean;
+Has_Empty  : Boolean;
+begin
+Examine_Array_Bounds (Typ, All_Static, Has_Empty);
+return All_Static and not Has_Empty;
+end Has_Static_Non_Empty_Array_Bounds;
 ----------------
 -- Has_Stream --
 ----------------
 return Present (Btyp)
 and then (Is_Record_Type (Btyp) or else Is_Array_Type (Btyp))
 and then Reverse_Storage_Order (Btyp);
 end In_Reverse_Storage_Order_Object;
+------------------------------
+-- In_Same_Declarative_Part --
+------------------------------
+function In_Same_Declarative_Part
+(Context : Node_Id;
+N       : Node_Id) return Boolean
+is
+Cont : Node_Id := Context;
+Nod  : Node_Id;
+begin
+if Nkind (Cont) = N_Compilation_Unit_Aux then
+Cont := Parent (Cont);
+end if;
+Nod := Parent (N);
+while Present (Nod) loop
+if Nod = Cont then
+return True;
+elsif Nkind_In (Nod, N_Accept_Statement,
+N_Block_Statement,
+N_Compilation_Unit,
+N_Entry_Body,
+N_Package_Body,
+N_Package_Declaration,
+N_Protected_Body,
+N_Subprogram_Body,
+N_Task_Body)
+then
+return False;
+elsif Nkind (Nod) = N_Subunit then
+Nod := Corresponding_Stub (Nod);
+else
+Nod := Parent (Nod);
+end if;
+end loop;
+return False;
+end In_Same_Declarative_Part;
 --------------------------------------
 -- In_Subprogram_Or_Concurrent_Unit --
 --------------------------------------
 function In_Subprogram_Or_Concurrent_Unit return Boolean is
 --  The type has no incomplete or private view
 return Empty;
 end Incomplete_Or_Partial_View;
+---------------------------------------
+-- Incomplete_View_From_Limited_With --
+---------------------------------------
+function Incomplete_View_From_Limited_With
+(Typ : Entity_Id) return Entity_Id
+is
+begin
+--  It might make sense to make this an attribute in Einfo, and set it
+--  in Sem_Ch10 in Build_Shadow_Entity. However, we're running short on
+--  slots for new attributes, and it seems a bit simpler to just search
+--  the Limited_View (if it exists) for an incomplete type whose
+--  Non_Limited_View is Typ.
+if Ekind (Scope (Typ)) = E_Package
+and then Present (Limited_View (Scope (Typ)))
+then
+declare
+Ent : Entity_Id := First_Entity (Limited_View (Scope (Typ)));
+begin
+while Present (Ent) loop
+if Ekind (Ent) in Incomplete_Kind
+and then Non_Limited_View (Ent) = Typ
+then
+return Ent;
+end if;
+Ent := Next_Entity (Ent);
+end loop;
+end;
+end if;
+return Typ;
+end Incomplete_View_From_Limited_With;
 ----------------------------------
 -- Indexed_Component_Bit_Offset --
 ----------------------------------
 else
 Set_First_Rep_Item (Typ, First_Rep_Item (From_Typ));
 end if;
 end if;
 end Inherit_Rep_Item_Chain;
+------------------------------------
+-- Inherits_From_Tagged_Full_View --
+------------------------------------
+function Inherits_From_Tagged_Full_View (Typ : Entity_Id) return Boolean is
+begin
+return Is_Private_Type (Typ)
+and then Present (Full_View (Typ))
+and then Is_Private_Type (Full_View (Typ))
+and then not Is_Tagged_Type (Full_View (Typ))
+and then Present (Underlying_Type (Full_View (Typ)))
+and then Is_Tagged_Type (Underlying_Type (Full_View (Typ)));
+end Inherits_From_Tagged_Full_View;
 ---------------------------------
 -- Insert_Explicit_Dereference --
 ---------------------------------
 Decl := Next (Decl);
 end loop;
 end Inspect_Deferred_Constant_Completion;
+-------------------------------
+-- Install_Elaboration_Model --
+-------------------------------
+procedure Install_Elaboration_Model (Unit_Id : Entity_Id) is
+function Find_Elaboration_Checks_Pragma (L : List_Id) return Node_Id;
+--  Try to find pragma Elaboration_Checks in arbitrary list L. Return
+--  Empty if there is no such pragma.
+------------------------------------
+-- Find_Elaboration_Checks_Pragma --
+------------------------------------
+function Find_Elaboration_Checks_Pragma (L : List_Id) return Node_Id is
+Item : Node_Id;
+begin
+Item := First (L);
+while Present (Item) loop
+if Nkind (Item) = N_Pragma
+and then Pragma_Name (Item) = Name_Elaboration_Checks
+then
+return Item;
+end if;
+Next (Item);
+end loop;
+return Empty;
+end Find_Elaboration_Checks_Pragma;
+--  Local variables
+Args  : List_Id;
+Model : Node_Id;
+Prag  : Node_Id;
+Unit  : Node_Id;
+--  Start of processing for Install_Elaboration_Model
+begin
+--  Nothing to do when the unit does not exist
+if No (Unit_Id) then
+return;
+end if;
+Unit := Parent (Unit_Declaration_Node (Unit_Id));
+--  Nothing to do when the unit is not a library unit
+if Nkind (Unit) /= N_Compilation_Unit then
+return;
+end if;
+Prag := Find_Elaboration_Checks_Pragma (Context_Items (Unit));
+--  The compilation unit is subject to pragma Elaboration_Checks. Set the
+--  elaboration model as specified by the pragma.
+if Present (Prag) then
+Args := Pragma_Argument_Associations (Prag);
+--  Guard against an illegal pragma. The sole argument must be an
+--  identifier which specifies either Dynamic or Static model.
+if Present (Args) then
+Model := Get_Pragma_Arg (First (Args));
+if Nkind (Model) = N_Identifier then
+Dynamic_Elaboration_Checks := Chars (Model) = Name_Dynamic;
+end if;
+end if;
+end if;
+end Install_Elaboration_Model;
 -----------------------------
 -- Install_Generic_Formals --
 -----------------------------
 procedure Install_Generic_Formals (Subp_Id : Entity_Id) is
 begin
 SPARK_Mode        := Mode;
 SPARK_Mode_Pragma := Prag;
 end Install_SPARK_Mode;
+--------------------------
+-- Invalid_Scalar_Value --
+--------------------------
+function Invalid_Scalar_Value
+(Loc      : Source_Ptr;
+Scal_Typ : Scalar_Id) return Node_Id
+is
+function Invalid_Binder_Value return Node_Id;
+--  Return a reference to the corresponding invalid value for type
+--  Scal_Typ as defined in unit System.Scalar_Values.
+function Invalid_Float_Value return Node_Id;
+--  Return the invalid value of float type Scal_Typ
+function Invalid_Integer_Value return Node_Id;
+--  Return the invalid value of integer type Scal_Typ
+procedure Set_Invalid_Binder_Values;
+--  Set the contents of collection Invalid_Binder_Values
+--------------------------
+-- Invalid_Binder_Value --
+--------------------------
+function Invalid_Binder_Value return Node_Id is
+Val_Id : Entity_Id;
+begin
+--  Initialize the collection of invalid binder values the first time
+--  around.
+Set_Invalid_Binder_Values;
+--  Obtain the corresponding variable from System.Scalar_Values which
+--  holds the invalid value for this type.
+Val_Id := Invalid_Binder_Values (Scal_Typ);
+pragma Assert (Present (Val_Id));
+return New_Occurrence_Of (Val_Id, Loc);
+end Invalid_Binder_Value;
+-------------------------
+-- Invalid_Float_Value --
+-------------------------
+function Invalid_Float_Value return Node_Id is
+Value : constant Ureal := Invalid_Floats (Scal_Typ);
+begin
+--  Pragma Invalid_Scalars did not specify an invalid value for this
+--  type. Fall back to the value provided by the binder.
+if Value = No_Ureal then
+return Invalid_Binder_Value;
+else
+return Make_Real_Literal (Loc, Realval => Value);
+end if;
+end Invalid_Float_Value;
+---------------------------
+-- Invalid_Integer_Value --
+---------------------------
+function Invalid_Integer_Value return Node_Id is
+Value : constant Uint := Invalid_Integers (Scal_Typ);
+begin
+--  Pragma Invalid_Scalars did not specify an invalid value for this
+--  type. Fall back to the value provided by the binder.
+if Value = No_Uint then
+return Invalid_Binder_Value;
+else
+return Make_Integer_Literal (Loc, Intval => Value);
+end if;
+end Invalid_Integer_Value;
+-------------------------------
+-- Set_Invalid_Binder_Values --
+-------------------------------
+procedure Set_Invalid_Binder_Values is
+begin
+if not Invalid_Binder_Values_Set then
+Invalid_Binder_Values_Set := True;
+--  Initialize the contents of the collection once since RTE calls
+--  are not cheap.
+Invalid_Binder_Values :=
+(Name_Short_Float     => RTE (RE_IS_Isf),
+Name_Float           => RTE (RE_IS_Ifl),
+Name_Long_Float      => RTE (RE_IS_Ilf),
+Name_Long_Long_Float => RTE (RE_IS_Ill),
+Name_Signed_8        => RTE (RE_IS_Is1),
+Name_Signed_16       => RTE (RE_IS_Is2),
+Name_Signed_32       => RTE (RE_IS_Is4),
+Name_Signed_64       => RTE (RE_IS_Is8),
+Name_Unsigned_8      => RTE (RE_IS_Iu1),
+Name_Unsigned_16     => RTE (RE_IS_Iu2),
+Name_Unsigned_32     => RTE (RE_IS_Iu4),
+Name_Unsigned_64     => RTE (RE_IS_Iu8));
+end if;
+end Set_Invalid_Binder_Values;
+--  Start of processing for Invalid_Scalar_Value
+begin
+if Scal_Typ in Float_Scalar_Id then
+return Invalid_Float_Value;
+else pragma Assert (Scal_Typ in Integer_Scalar_Id);
+return Invalid_Integer_Value;
+end if;
+end Invalid_Scalar_Value;
 -----------------------------
 -- Is_Actual_Out_Parameter --
 -----------------------------
 function Is_Actual_Out_Parameter (N : Node_Id) return Boolean is
 ----------------------
 -- Is_Atomic_Object --
 ----------------------
 function Is_Atomic_Object (N : Node_Id) return Boolean is
+function Is_Atomic_Entity (Id : Entity_Id) return Boolean;
-function Object_Has_Atomic_Components (N : Node_Id) return Boolean;
+pragma Inline (Is_Atomic_Entity);
---  Determines if given object has atomic components
+--  Determine whether arbitrary entity Id is either atomic or has atomic
+--  components.
-function Is_Atomic_Prefix (N : Node_Id) return Boolean;
---  If prefix is an implicit dereference, examine designated type
+function Is_Atomic_Prefix (Pref : Node_Id) return Boolean;
+--  Determine whether prefix Pref of an indexed or selected component is
+--  an atomic object.
+----------------------
+-- Is_Atomic_Entity --
+----------------------
+function Is_Atomic_Entity (Id : Entity_Id) return Boolean is
+begin
+return Is_Atomic (Id) or else Has_Atomic_Components (Id);
+end Is_Atomic_Entity;
 ----------------------
 -- Is_Atomic_Prefix --
 ----------------------
-function Is_Atomic_Prefix (N : Node_Id) return Boolean is
+function Is_Atomic_Prefix (Pref : Node_Id) return Boolean is
+Typ : constant Entity_Id := Etype (Pref);
 begin
-if Is_Access_Type (Etype (N)) then
+if Is_Access_Type (Typ) then
-return
+return Has_Atomic_Components (Designated_Type (Typ));
-Has_Atomic_Components (Designated_Type (Etype (N)));
-else
+elsif Is_Atomic_Entity (Typ) then
-return Object_Has_Atomic_Components (N);
+return True;
-end if;
-end Is_Atomic_Prefix;
+elsif Is_Entity_Name (Pref)
+and then Is_Atomic_Entity (Entity (Pref))
-----------------------------------
--- Object_Has_Atomic_Components --
-----------------------------------
-function Object_Has_Atomic_Components (N : Node_Id) return Boolean is
-begin
-if Has_Atomic_Components (Etype (N))
-or else Is_Atomic (Etype (N))
 then
 return True;
-elsif Is_Entity_Name (N)
+elsif Nkind (Pref) = N_Indexed_Component then
-and then (Has_Atomic_Components (Entity (N))
+return Is_Atomic_Prefix (Prefix (Pref));
-or else Is_Atomic (Entity (N)))
-then
+elsif Nkind (Pref) = N_Selected_Component then
-return True;
+return
+Is_Atomic_Prefix (Prefix (Pref))
-elsif Nkind (N) = N_Selected_Component
+or else Is_Atomic (Entity (Selector_Name (Pref)));
-and then Is_Atomic (Entity (Selector_Name (N)))
+end if;
-then
-return True;
+return False;
+end Is_Atomic_Prefix;
-elsif Nkind (N) = N_Indexed_Component
-or else Nkind (N) = N_Selected_Component
-then
-return Is_Atomic_Prefix (Prefix (N));
-else
-return False;
-end if;
-end Object_Has_Atomic_Components;
 --  Start of processing for Is_Atomic_Object
 begin
---  Predicate is not relevant to subprograms
+if Is_Entity_Name (N) then
+return Is_Atomic_Object_Entity (Entity (N));
-if Is_Entity_Name (N) and then Is_Overloadable (Entity (N)) then
-return False;
+elsif Nkind (N) = N_Indexed_Component then
+return Is_Atomic (Etype (N)) or else Is_Atomic_Prefix (Prefix (N));
-elsif Is_Atomic (Etype (N))
-or else (Is_Entity_Name (N) and then Is_Atomic (Entity (N)))
+elsif Nkind (N) = N_Selected_Component then
-then
+return
-return True;
+Is_Atomic (Etype (N))
+or else Is_Atomic_Prefix (Prefix (N))
-elsif Nkind (N) = N_Selected_Component
+or else Is_Atomic (Entity (Selector_Name (N)));
-and then Is_Atomic (Entity (Selector_Name (N)))
+end if;
-then
-return True;
+return False;
-elsif Nkind (N) = N_Indexed_Component
-or else Nkind (N) = N_Selected_Component
-then
-return Is_Atomic_Prefix (Prefix (N));
-else
-return False;
-end if;
 end Is_Atomic_Object;
+-----------------------------
+-- Is_Atomic_Object_Entity --
+-----------------------------
+function Is_Atomic_Object_Entity (Id : Entity_Id) return Boolean is
+begin
+return
+Is_Object (Id)
+and then (Is_Atomic (Id) or else Is_Atomic (Etype (Id)));
+end Is_Atomic_Object_Entity;
 -----------------------------
 -- Is_Atomic_Or_VFA_Object --
 -----------------------------
 -- Is_Body_Or_Package_Declaration --
 ------------------------------------
 function Is_Body_Or_Package_Declaration (N : Node_Id) return Boolean is
 begin
-return Nkind_In (N, N_Entry_Body,
+return Is_Body (N) or else Nkind (N) = N_Package_Declaration;
-N_Package_Body,
-N_Package_Declaration,
-N_Protected_Body,
-N_Subprogram_Body,
-N_Task_Body);
 end Is_Body_Or_Package_Declaration;
 -----------------------
 -- Is_Bounded_String --
 -----------------------
 E_Entry_Family,
 E_Function,
 E_Package,
 E_Procedure,
 E_Protected_Type,
-E_Task_Type));
+E_Task_Type)
+or else
+Is_Record_Type (Context_Id));
 return Scope_Within_Or_Same (Context_Id, Ref_Id);
 end if;
 end Is_CCT_Instance;
 -------------------------
 begin
 if Ekind (Proc_Nam) = E_Procedure
 and then Present (Parameter_Specifications (Parent (Proc_Nam)))
 then
-Param := Parameter_Type (First (
+Param :=
-Parameter_Specifications (Parent (Proc_Nam))));
+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;
 --  In the case where an Itype was created for a dispatchin call, the
 Typ : constant Entity_Id := Entity (N);
 P   : Node_Id;
 begin
 --  Simplest case: entity is a concurrent type and we are currently
---  inside the body. This will eventually be expanded into a
+--  inside the body. This will eventually be expanded into a call to
---  call to Self (for tasks) or _object (for protected objects).
+--  Self (for tasks) or _object (for protected objects).
 if Is_Concurrent_Type (Typ) and then In_Open_Scopes (Typ) then
 return True;
 else
 and then Nkind (Parent (P)) = N_Subtype_Declaration
 then
 return True;
 elsif Nkind (P) = N_Pragma
-and then
+and then Get_Pragma_Id (P) = Pragma_Predicate_Failure
-Get_Pragma_Id (P) = Pragma_Predicate_Failure
 then
 return True;
 end if;
 P := Parent (P);
 --------------------
 -- Is_Declaration --
 --------------------
-function Is_Declaration (N : Node_Id) return Boolean is
+function Is_Declaration
-begin
+(N                : Node_Id;
-return
+Body_OK          : Boolean := True;
-Is_Declaration_Other_Than_Renaming (N)
+Concurrent_OK    : Boolean := True;
-or else Is_Renaming_Declaration (N);
+Formal_OK        : Boolean := True;
-end Is_Declaration;
+Generic_OK       : Boolean := True;
+Instantiation_OK : Boolean := True;
-----------------------------------------
+Renaming_OK      : Boolean := True;
--- Is_Declaration_Other_Than_Renaming --
+Stub_OK          : Boolean := True;
-----------------------------------------
+Subprogram_OK    : Boolean := True;
+Type_OK          : Boolean := True) return Boolean
-function Is_Declaration_Other_Than_Renaming (N : Node_Id) return Boolean is
+is
 begin
 case Nkind (N) is
+--  Body declarations
+when N_Proper_Body =>
+return Body_OK;
+--  Concurrent type declarations
+when N_Protected_Type_Declaration
+| N_Single_Protected_Declaration
+| N_Single_Task_Declaration
+| N_Task_Type_Declaration
+=>
+return Concurrent_OK or Type_OK;
+--  Formal declarations
+when N_Formal_Abstract_Subprogram_Declaration
+| N_Formal_Concrete_Subprogram_Declaration
+| N_Formal_Object_Declaration
+| N_Formal_Package_Declaration
+| N_Formal_Type_Declaration
+=>
+return Formal_OK;
+--  Generic declarations
+when N_Generic_Package_Declaration
+| N_Generic_Subprogram_Declaration
+=>
+return Generic_OK;
+--  Generic instantiations
+when N_Function_Instantiation
+| N_Package_Instantiation
+| N_Procedure_Instantiation
+=>
+return Instantiation_OK;
+--  Generic renaming declarations
+when N_Generic_Renaming_Declaration =>
+return Generic_OK or Renaming_OK;
+--  Renaming declarations
+when N_Exception_Renaming_Declaration
+| N_Object_Renaming_Declaration
+| N_Package_Renaming_Declaration
+| N_Subprogram_Renaming_Declaration
+=>
+return Renaming_OK;
+--  Stub declarations
+when N_Body_Stub =>
+return Stub_OK;
+--  Subprogram declarations
 when N_Abstract_Subprogram_Declaration
+| N_Entry_Declaration
+| N_Expression_Function
+| N_Subprogram_Declaration
+=>
+return Subprogram_OK;
+--  Type declarations
+when N_Full_Type_Declaration
+| N_Incomplete_Type_Declaration
+| N_Private_Extension_Declaration
+| N_Private_Type_Declaration
+| N_Subtype_Declaration
+=>
+return Type_OK;
+--  Miscellaneous
+when N_Component_Declaration
 | N_Exception_Declaration
-| N_Expression_Function
+| N_Implicit_Label_Declaration
-| N_Full_Type_Declaration
-| N_Generic_Package_Declaration
-| N_Generic_Subprogram_Declaration
 | N_Number_Declaration
 | N_Object_Declaration
 | N_Package_Declaration
-| N_Private_Extension_Declaration
-| N_Private_Type_Declaration
-| N_Subprogram_Declaration
-| N_Subtype_Declaration
 =>
 return True;
 when others =>
 return False;
 end case;
-end Is_Declaration_Other_Than_Renaming;
+end Is_Declaration;
 --------------------------------
 -- Is_Declared_Within_Variant --
 --------------------------------
 when others =>
 return False;
 end case;
 end Is_Name_Reference;
+------------------------------------
+-- Is_Non_Preelaborable_Construct --
+------------------------------------
+function Is_Non_Preelaborable_Construct (N : Node_Id) return Boolean is
+--  NOTE: the routines within Is_Non_Preelaborable_Construct are
+--  intentionally unnested to avoid deep indentation of code.
+Non_Preelaborable : exception;
+--  This exception is raised when the construct violates preelaborability
+--  to terminate the recursion.
+procedure Visit (Nod : Node_Id);
+--  Semantically inspect construct Nod to determine whether it violates
+--  preelaborability. This routine raises Non_Preelaborable.
+procedure Visit_List (List : List_Id);
+pragma Inline (Visit_List);
+--  Invoke Visit on each element of list List. This routine raises
+--  Non_Preelaborable.
+procedure Visit_Pragma (Prag : Node_Id);
+pragma Inline (Visit_Pragma);
+--  Semantically inspect pragma Prag to determine whether it violates
+--  preelaborability. This routine raises Non_Preelaborable.
+procedure Visit_Subexpression (Expr : Node_Id);
+pragma Inline (Visit_Subexpression);
+--  Semantically inspect expression Expr to determine whether it violates
+--  preelaborability. This routine raises Non_Preelaborable.
+-----------
+-- Visit --
+-----------
+procedure Visit (Nod : Node_Id) is
+begin
+case Nkind (Nod) is
+--  Declarations
+when N_Component_Declaration =>
+--  Defining_Identifier is left out because it is not relevant
+--  for preelaborability.
+Visit (Component_Definition (Nod));
+Visit (Expression (Nod));
+when N_Derived_Type_Definition =>
+--  Interface_List is left out because it is not relevant for
+--  preelaborability.
+Visit (Record_Extension_Part (Nod));
+Visit (Subtype_Indication (Nod));
+when N_Entry_Declaration =>
+--  A protected type with at leat one entry is not preelaborable
+--  while task types are never preelaborable. This renders entry
+--  declarations non-preelaborable.
+raise Non_Preelaborable;
+when N_Full_Type_Declaration =>
+--  Defining_Identifier and Discriminant_Specifications are left
+--  out because they are not relevant for preelaborability.
+Visit (Type_Definition (Nod));
+when N_Function_Instantiation
+| N_Package_Instantiation
+| N_Procedure_Instantiation
+=>
+--  Defining_Unit_Name and Name are left out because they are
+--  not relevant for preelaborability.
+Visit_List (Generic_Associations (Nod));
+when N_Object_Declaration =>
+--  Defining_Identifier is left out because it is not relevant
+--  for preelaborability.
+Visit (Object_Definition (Nod));
+if Has_Init_Expression (Nod) then
+Visit (Expression (Nod));
+elsif not Has_Preelaborable_Initialization
+(Etype (Defining_Entity (Nod)))
+then
+raise Non_Preelaborable;
+end if;
+when N_Private_Extension_Declaration
+| N_Subtype_Declaration
+=>
+--  Defining_Identifier, Discriminant_Specifications, and
+--  Interface_List are left out because they are not relevant
+--  for preelaborability.
+Visit (Subtype_Indication (Nod));
+when N_Protected_Type_Declaration
+| N_Single_Protected_Declaration
+=>
+--  Defining_Identifier, Discriminant_Specifications, and
+--  Interface_List are left out because they are not relevant
+--  for preelaborability.
+Visit (Protected_Definition (Nod));
+--  A [single] task type is never preelaborable
+when N_Single_Task_Declaration
+| N_Task_Type_Declaration
+=>
+raise Non_Preelaborable;
+--  Pragmas
+when N_Pragma =>
+Visit_Pragma (Nod);
+--  Statements
+when N_Statement_Other_Than_Procedure_Call =>
+if Nkind (Nod) /= N_Null_Statement then
+raise Non_Preelaborable;
+end if;
+--  Subexpressions
+when N_Subexpr =>
+Visit_Subexpression (Nod);
+--  Special
+when N_Access_To_Object_Definition =>
+Visit (Subtype_Indication (Nod));
+when N_Case_Expression_Alternative =>
+Visit (Expression (Nod));
+Visit_List (Discrete_Choices (Nod));
+when N_Component_Definition =>
+Visit (Access_Definition (Nod));
+Visit (Subtype_Indication (Nod));
+when N_Component_List =>
+Visit_List (Component_Items (Nod));
+Visit (Variant_Part (Nod));
+when N_Constrained_Array_Definition =>
+Visit_List (Discrete_Subtype_Definitions (Nod));
+Visit (Component_Definition (Nod));
+when N_Delta_Constraint
+| N_Digits_Constraint
+=>
+--  Delta_Expression and Digits_Expression are left out because
+--  they are not relevant for preelaborability.
+Visit (Range_Constraint (Nod));
+when N_Discriminant_Specification =>
+--  Defining_Identifier and Expression are left out because they
+--  are not relevant for preelaborability.
+Visit (Discriminant_Type (Nod));
+when N_Generic_Association =>
+--  Selector_Name is left out because it is not relevant for
+--  preelaborability.
+Visit (Explicit_Generic_Actual_Parameter (Nod));
+when N_Index_Or_Discriminant_Constraint =>
+Visit_List (Constraints (Nod));
+when N_Iterator_Specification =>
+--  Defining_Identifier is left out because it is not relevant
+--  for preelaborability.
+Visit (Name (Nod));
+Visit (Subtype_Indication (Nod));
+when N_Loop_Parameter_Specification =>
+--  Defining_Identifier is left out because it is not relevant
+--  for preelaborability.
+Visit (Discrete_Subtype_Definition (Nod));
+when N_Protected_Definition =>
+--  End_Label is left out because it is not relevant for
+--  preelaborability.
+Visit_List (Private_Declarations (Nod));
+Visit_List (Visible_Declarations (Nod));
+when N_Range_Constraint =>
+Visit (Range_Expression (Nod));
+when N_Record_Definition
+| N_Variant
+=>
+--  End_Label, Discrete_Choices, and Interface_List are left out
+--  because they are not relevant for preelaborability.
+Visit (Component_List (Nod));
+when N_Subtype_Indication =>
+--  Subtype_Mark is left out because it is not relevant for
+--  preelaborability.
+Visit (Constraint (Nod));
+when N_Unconstrained_Array_Definition =>
+--  Subtype_Marks is left out because it is not relevant for
+--  preelaborability.
+Visit (Component_Definition (Nod));
+when N_Variant_Part =>
+--  Name is left out because it is not relevant for
+--  preelaborability.
+Visit_List (Variants (Nod));
+--  Default
+when others =>
+null;
+end case;
+end Visit;
+----------------
+-- Visit_List --
+----------------
+procedure Visit_List (List : List_Id) is
+Nod : Node_Id;
+begin
+if Present (List) then
+Nod := First (List);
+while Present (Nod) loop
+Visit (Nod);
+Next (Nod);
+end loop;
+end if;
+end Visit_List;
+------------------
+-- Visit_Pragma --
+------------------
+procedure Visit_Pragma (Prag : Node_Id) is
+begin
+case Get_Pragma_Id (Prag) is
+when Pragma_Assert
+| Pragma_Assert_And_Cut
+| Pragma_Assume
+| Pragma_Async_Readers
+| Pragma_Async_Writers
+| Pragma_Attribute_Definition
+| Pragma_Check
+| Pragma_Constant_After_Elaboration
+| Pragma_CPU
+| Pragma_Deadline_Floor
+| Pragma_Dispatching_Domain
+| Pragma_Effective_Reads
+| Pragma_Effective_Writes
+| Pragma_Extensions_Visible
+| Pragma_Ghost
+| Pragma_Secondary_Stack_Size
+| Pragma_Task_Name
+| Pragma_Volatile_Function
+=>
+Visit_List (Pragma_Argument_Associations (Prag));
+--  Default
+when others =>
+null;
+end case;
+end Visit_Pragma;
+-------------------------
+-- Visit_Subexpression --
+-------------------------
+procedure Visit_Subexpression (Expr : Node_Id) is
+procedure Visit_Aggregate (Aggr : Node_Id);
+pragma Inline (Visit_Aggregate);
+--  Semantically inspect aggregate Aggr to determine whether it
+--  violates preelaborability.
+---------------------
+-- Visit_Aggregate --
+---------------------
+procedure Visit_Aggregate (Aggr : Node_Id) is
+begin
+if not Is_Preelaborable_Aggregate (Aggr) then
+raise Non_Preelaborable;
+end if;
+end Visit_Aggregate;
+--  Start of processing for Visit_Subexpression
+begin
+case Nkind (Expr) is
+when N_Allocator
+| N_Qualified_Expression
+| N_Type_Conversion
+| N_Unchecked_Expression
+| N_Unchecked_Type_Conversion
+=>
+--  Subpool_Handle_Name and Subtype_Mark are left out because
+--  they are not relevant for preelaborability.
+Visit (Expression (Expr));
+when N_Aggregate
+| N_Extension_Aggregate
+=>
+Visit_Aggregate (Expr);
+when N_Attribute_Reference
+| N_Explicit_Dereference
+| N_Reference
+=>
+--  Attribute_Name and Expressions are left out because they are
+--  not relevant for preelaborability.
+Visit (Prefix (Expr));
+when N_Case_Expression =>
+--  End_Span is left out because it is not relevant for
+--  preelaborability.
+Visit_List (Alternatives (Expr));
+Visit (Expression (Expr));
+when N_Delta_Aggregate =>
+Visit_Aggregate (Expr);
+Visit (Expression (Expr));
+when N_Expression_With_Actions =>
+Visit_List (Actions (Expr));
+Visit (Expression (Expr));
+when N_If_Expression =>
+Visit_List (Expressions (Expr));
+when N_Quantified_Expression =>
+Visit (Condition (Expr));
+Visit (Iterator_Specification (Expr));
+Visit (Loop_Parameter_Specification (Expr));
+when N_Range =>
+Visit (High_Bound (Expr));
+Visit (Low_Bound (Expr));
+when N_Slice =>
+Visit (Discrete_Range (Expr));
+Visit (Prefix (Expr));
+--  Default
+when others =>
+--  The evaluation of an object name is not preelaborable,
+--  unless the name is a static expression (checked further
+--  below), or statically denotes a discriminant.
+if Is_Entity_Name (Expr) then
+Object_Name : declare
+Id : constant Entity_Id := Entity (Expr);
+begin
+if Is_Object (Id) then
+if Ekind (Id) = E_Discriminant then
+null;
+elsif Ekind_In (Id, E_Constant, E_In_Parameter)
+and then Present (Discriminal_Link (Id))
+then
+null;
+else
+raise Non_Preelaborable;
+end if;
+end if;
+end Object_Name;
+--  A non-static expression is not preelaborable
+elsif not Is_OK_Static_Expression (Expr) then
+raise Non_Preelaborable;
+end if;
+end case;
+end Visit_Subexpression;
+--  Start of processing for Is_Non_Preelaborable_Construct
+begin
+Visit (N);
+--  At this point it is known that the construct is preelaborable
+return False;
+exception
+--  The elaboration of the construct performs an action which violates
+--  preelaborability.
+when Non_Preelaborable =>
+return True;
+end Is_Non_Preelaborable_Construct;
 ---------------------------------
 -- Is_Nontrivial_DIC_Procedure --
 ---------------------------------
 function Is_Nontrivial_DIC_Procedure (Id : Entity_Id) return Boolean is
 --  If this node is rewritten, then test the original form, if that is
 --  OK, then we consider the rewritten node OK (for example, if the
 --  original node is a conversion, then Is_Variable will not be true
 --  but we still want to allow the conversion if it converts a variable).
-elsif Original_Node (AV) /= AV then
+elsif Is_Rewrite_Substitution (AV) then
 --  In Ada 2012, the explicit dereference may be a rewritten call to a
 --  Reference function.
 if Ada_Version >= Ada_2012
 --  entry, function, or procedure in prefixed form where the prefix is
 --  Obj_Ref.
 function Within_Check (Nod : Node_Id) return Boolean;
 --  Determine whether an arbitrary node appears in a check node
-function Within_Subprogram_Call (Nod : Node_Id) return Boolean;
---  Determine whether an arbitrary node appears in an entry, function, or
---  procedure call.
 function Within_Volatile_Function (Id : Entity_Id) return Boolean;
 --  Determine whether an arbitrary entity appears in a volatile function
 ---------------------------------
 end loop;
 return False;
 end Within_Check;
-----------------------------
--- Within_Subprogram_Call --
-----------------------------
-function Within_Subprogram_Call (Nod : Node_Id) return Boolean is
-Par : Node_Id;
-begin
---  Climb the parent chain looking for a function or procedure call
-Par := Nod;
-while Present (Par) loop
-if Nkind_In (Par, N_Entry_Call_Statement,
-N_Function_Call,
-N_Procedure_Call_Statement)
-then
-return True;
---  Prevent the search from going too far
-elsif Is_Body_Or_Package_Declaration (Par) then
-exit;
-end if;
-Par := Parent (Par);
-end loop;
-return False;
-end Within_Subprogram_Call;
 ------------------------------
 -- Within_Volatile_Function --
 ------------------------------
 function Within_Volatile_Function (Id : Entity_Id) return Boolean is
 Obj_Ref => Context)
 then
 return True;
 --  The volatile object appears as the prefix of attributes Address,
---  Alignment, Component_Size, First_Bit, Last_Bit, Position, Size,
+--  Alignment, Component_Size, First, First_Bit, Last, Last_Bit, Length,
---  Storage_Size.
+--  Position, Size, Storage_Size.
 elsif Nkind (Context) = N_Attribute_Reference
 and then Prefix (Context) = Obj_Ref
 and then Nam_In (Attribute_Name (Context), Name_Address,
 Name_Alignment,
 Name_Component_Size,
+Name_First,
 Name_First_Bit,
+Name_Last,
 Name_Last_Bit,
+Name_Length,
 Name_Position,
 Name_Size,
 Name_Storage_Size)
 then
 return True;
 Par  : Node_Id;
 Expr : Node_Id;
 begin
 Expr := N;
-Par  := Parent (N);
+Par  := N;
 --  A postcondition whose expression is a short-circuit is broken down
 --  into individual aspects for better exception reporting. The original
 --  short-circuit expression is rewritten as the second operand, and an
 --  occurrence of 'Old in that operand is potentially unevaluated.
---  See Sem_ch13.adb for details of this transformation.
+--  See sem_ch13.adb for details of this transformation. The reference
+--  to 'Old may appear within an expression, so we must look for the
-if Nkind (Original_Node (Par)) = N_And_Then then
+--  enclosing pragma argument in the tree that contains the reference.
-return True;
-end if;
+while Present (Par)
+and then Nkind (Par) /= N_Pragma_Argument_Association
-while not Nkind_In (Par, N_If_Expression,
+loop
+if Is_Rewrite_Substitution (Par)
+and then Nkind (Original_Node (Par)) = N_And_Then
+then
+return True;
+end if;
+Par := Parent (Par);
+end loop;
+--  Other cases; 'Old appears within other expression (not the top-level
+--  conjunct in a postcondition) with a potentially unevaluated operand.
+Par := Parent (Expr);
+while not Nkind_In (Par, N_And_Then,
 N_Case_Expression,
-N_And_Then,
+N_If_Expression,
-N_Or_Else,
 N_In,
 N_Not_In,
+N_Or_Else,
 N_Quantified_Expression)
 loop
 Expr := Par;
 Par  := Parent (Par);
 else
 return False;
 end if;
 end Is_Potentially_Unevaluated;
+-----------------------------------------
+-- Is_Predefined_Dispatching_Operation --
+-----------------------------------------
+function Is_Predefined_Dispatching_Operation
+(E : Entity_Id) return Boolean
+is
+TSS_Name : TSS_Name_Type;
+begin
+if not Is_Dispatching_Operation (E) then
+return False;
+end if;
+Get_Name_String (Chars (E));
+--  Most predefined primitives have internally generated names. Equality
+--  must be treated differently; the predefined operation is recognized
+--  as a homogeneous binary operator that returns Boolean.
+if Name_Len > TSS_Name_Type'Last then
+TSS_Name :=
+TSS_Name_Type
+(Name_Buffer (Name_Len - TSS_Name'Length + 1 .. Name_Len));
+if Nam_In (Chars (E), Name_uAssign, Name_uSize)
+or else
+(Chars (E) = Name_Op_Eq
+and then Etype (First_Formal (E)) = Etype (Last_Formal (E)))
+or else TSS_Name = TSS_Deep_Adjust
+or else TSS_Name = TSS_Deep_Finalize
+or else TSS_Name = TSS_Stream_Input
+or else TSS_Name = TSS_Stream_Output
+or else TSS_Name = TSS_Stream_Read
+or else TSS_Name = TSS_Stream_Write
+or else Is_Predefined_Interface_Primitive (E)
+then
+return True;
+end if;
+end if;
+return False;
+end Is_Predefined_Dispatching_Operation;
+---------------------------------------
+-- Is_Predefined_Interface_Primitive --
+---------------------------------------
+function Is_Predefined_Interface_Primitive (E : Entity_Id) return Boolean is
+begin
+--  In VM targets we don't restrict the functionality of this test to
+--  compiling in Ada 2005 mode since in VM targets any tagged type has
+--  these primitives.
+return (Ada_Version >= Ada_2005 or else not Tagged_Type_Expansion)
+and then Nam_In (Chars (E), Name_uDisp_Asynchronous_Select,
+Name_uDisp_Conditional_Select,
+Name_uDisp_Get_Prim_Op_Kind,
+Name_uDisp_Get_Task_Id,
+Name_uDisp_Requeue,
+Name_uDisp_Timed_Select);
+end Is_Predefined_Interface_Primitive;
+---------------------------------------
+-- Is_Predefined_Internal_Operation  --
+---------------------------------------
+function Is_Predefined_Internal_Operation
+(E : Entity_Id) return Boolean
+is
+TSS_Name : TSS_Name_Type;
+begin
+if not Is_Dispatching_Operation (E) then
+return False;
+end if;
+Get_Name_String (Chars (E));
+--  Most predefined primitives have internally generated names. Equality
+--  must be treated differently; the predefined operation is recognized
+--  as a homogeneous binary operator that returns Boolean.
+if Name_Len > TSS_Name_Type'Last then
+TSS_Name :=
+TSS_Name_Type
+(Name_Buffer (Name_Len - TSS_Name'Length + 1 .. Name_Len));
+if Nam_In (Chars (E), Name_uSize, Name_uAssign)
+or else
+(Chars (E) = Name_Op_Eq
+and then Etype (First_Formal (E)) = Etype (Last_Formal (E)))
+or else TSS_Name = TSS_Deep_Adjust
+or else TSS_Name = TSS_Deep_Finalize
+or else Is_Predefined_Interface_Primitive (E)
+then
+return True;
+end if;
+end if;
+return False;
+end Is_Predefined_Internal_Operation;
 --------------------------------
 -- Is_Preelaborable_Aggregate --
 --------------------------------
 function Is_Preelaborable_Aggregate (Aggr : Node_Id) return Boolean is
 Array_Aggr : constant Boolean   := Is_Array_Type (Aggr_Typ);
 Anc_Part : Node_Id;
 Assoc    : Node_Id;
 Choice   : Node_Id;
-Comp_Typ : Entity_Id;
+Comp_Typ : Entity_Id := Empty; -- init to avoid warning
 Expr     : Node_Id;
 begin
 if Array_Aggr then
 Comp_Typ := Component_Type (Aggr_Typ);
 end loop;
 --  The type of the choice must have preelaborable initialization if
 --  the association carries a <>.
+pragma Assert (Present (Comp_Typ));
 if Box_Present (Assoc) then
 if not Has_Preelaborable_Initialization (Comp_Typ) then
 return False;
 end if;
 return Nkind (N) = N_Subprogram_Body_Stub
 and then Ekind (Defining_Entity (N)) /= E_Subprogram_Body;
 end Is_Subprogram_Stub_Without_Prior_Declaration;
+---------------------------
+-- Is_Suitable_Primitive --
+---------------------------
+function Is_Suitable_Primitive (Subp_Id : Entity_Id) return Boolean is
+begin
+--  The Default_Initial_Condition and invariant procedures must not be
+--  treated as primitive operations even when they apply to a tagged
+--  type. These routines must not act as targets of dispatching calls
+--  because they already utilize class-wide-precondition semantics to
+--  handle inheritance and overriding.
+if Ekind (Subp_Id) = E_Procedure
+and then (Is_DIC_Procedure (Subp_Id)
+or else
+Is_Invariant_Procedure (Subp_Id))
+then
+return False;
+end if;
+return True;
+end Is_Suitable_Primitive;
 --------------------------
 -- Is_Suspension_Object --
 --------------------------
 function Is_Suspension_Object (Id : Entity_Id) return Boolean is
 return True;
 --  The object is synchronized if it is atomic and Async_Writers is
 --  enabled.
-elsif Is_Atomic (Id) and then Async_Writers_Enabled (Id) then
+elsif Is_Atomic_Object_Entity (Id)
+and then Async_Writers_Enabled (Id)
+then
 return True;
 --  A constant is a synchronized object by default
 elsif Ekind (Id) = E_Constant then
 Comp_Typ : Entity_Id;
 begin
 pragma Assert (Is_Record_Type (E));
-Comp := First_Entity (E);
+Comp := First_Component (E);
 while Present (Comp) loop
-Comp_Typ := Etype (Comp);
+Comp_Typ := Underlying_Type (Etype (Comp));
 --  Recursive call if the record type has discriminants
 if Is_Record_Type (Comp_Typ)
 and then Has_Discriminants (Comp_Typ)
 and then Is_Variable_Size_Array (Comp_Typ)
 then
 return True;
 end if;
-Next_Entity (Comp);
+Next_Component (Comp);
 end loop;
 return False;
 end Is_Variable_Size_Record;
 declare
 E : constant Entity_Id := Entity (Orig_Node);
 K : constant Entity_Kind := Ekind (E);
 begin
+if Is_Loop_Parameter (E) then
+return False;
+end if;
 return    (K = E_Variable
 and then Nkind (Parent (E)) /= N_Exception_Handler)
 or else (K = E_Component
 and then not In_Protected_Function (E))
 or else K = E_Out_Parameter
 return False;
 end case;
 end if;
 end Is_Variable;
-------------------------------
--- Is_Verifiable_DIC_Pragma --
-------------------------------
-function Is_Verifiable_DIC_Pragma (Prag : Node_Id) return Boolean is
-Args : constant List_Id := Pragma_Argument_Associations (Prag);
-begin
---  To qualify as verifiable, a DIC pragma must have a non-null argument
-return
-Present (Args)
-and then Nkind (Get_Pragma_Arg (First (Args))) /= N_Null;
-end Is_Verifiable_DIC_Pragma;
 ---------------------------
 -- Is_Visibly_Controlled --
 ---------------------------
 function Is_Visibly_Controlled (T : Entity_Id) return Boolean is
 -----------------------------
 -- Iterate_Call_Parameters --
 -----------------------------
 procedure Iterate_Call_Parameters (Call : Node_Id) is
+Actual : Node_Id   := First_Actual (Call);
 Formal : Entity_Id := First_Formal (Get_Called_Entity (Call));
-Actual : Node_Id   := First_Actual (Call);
 begin
 while Present (Formal) and then Present (Actual) loop
 Handle_Parameter (Formal, Actual);
-Formal := Next_Formal (Formal);
-Actual := Next_Actual (Actual);
+Next_Formal (Formal);
+Next_Actual (Actual);
 end loop;
+pragma Assert (No (Formal));
+pragma Assert (No (Actual));
 end Iterate_Call_Parameters;
 ---------------------------
 -- Itype_Has_Declaration --
 ---------------------------
 function Mark_Allocator (N : Node_Id) return Traverse_Result is
 begin
 if Nkind (N) = N_Allocator then
 if Is_Dynamic then
+Set_Is_Static_Coextension (N, False);
 Set_Is_Dynamic_Coextension (N);
 --  If the allocator expression is potentially dynamic, it may
 --  be expanded out of order and require dynamic allocation
 --  anyway, so we treat the coextension itself as dynamic.
 --  Potential optimization ???
 elsif Nkind (Expression (N)) = N_Qualified_Expression
 and then Nkind (Expression (Expression (N))) = N_Op_Concat
 then
+Set_Is_Static_Coextension (N, False);
 Set_Is_Dynamic_Coextension (N);
 else
+Set_Is_Dynamic_Coextension (N, False);
 Set_Is_Static_Coextension (N);
 end if;
 end if;
 return OK;
 ---------------------------------
 -- Mark_Elaboration_Attributes --
 ---------------------------------
 procedure Mark_Elaboration_Attributes
-(N_Id   : Node_Or_Entity_Id;
+(N_Id     : Node_Or_Entity_Id;
-Checks : Boolean := False;
+Checks   : Boolean := False;
-Level  : Boolean := False;
+Level    : Boolean := False;
-Modes  : Boolean := False)
+Modes    : Boolean := False;
+Warnings : Boolean := False)
 is
 function Elaboration_Checks_OK
 (Target_Id  : Entity_Id;
 Context_Id : Entity_Id) return Boolean;
 --  Determine whether elaboration checks are enabled for target Target_Id
 if Checks and then not Is_Elaboration_Checks_OK_Id (Id) then
 Set_Is_Elaboration_Checks_OK_Id (Id,
 Elaboration_Checks_OK
 (Target_Id  => Id,
 Context_Id => Scope (Id)));
+end if;
---  Entities do not need to capture their enclosing level. The Ghost
---  and SPARK modes in effect are already marked during analysis.
+--  Mark the status of elaboration warnings in effect. Do not reset
+--  the status in case the entity is reanalyzed with warnings off.
-else
-null;
+if Warnings and then not Is_Elaboration_Warnings_OK_Id (Id) then
+Set_Is_Elaboration_Warnings_OK_Id (Id, Elab_Warnings);
 end if;
 end Mark_Elaboration_Attributes_Id;
 --------------------------------------
 -- Mark_Elaboration_Attributes_Node --
 if SPARK_Mode = On then
 Set_Is_SPARK_Mode_On_Node (N);
 end if;
 end if;
+--  Mark the status of elaboration warnings in effect. Do not reset
+--  the status in case the node is reanalyzed with warnings off.
+if Warnings and then not Is_Elaboration_Warnings_OK_Node (N) then
+Set_Is_Elaboration_Warnings_OK_Node (N, Elab_Warnings);
+end if;
 end Mark_Elaboration_Attributes_Node;
 --  Start of processing for Mark_Elaboration_Attributes
 begin
+--  Do not capture any elaboration-related attributes when switch -gnatH
+--  (legacy elaboration checking mode enabled) is in effect because the
+--  attributes are useless to the legacy model.
+if Legacy_Elaboration_Checks then
+return;
+end if;
 if Nkind (N_Id) in N_Entity then
 Mark_Elaboration_Attributes_Id (N_Id);
 else
 Mark_Elaboration_Attributes_Node (N_Id);
 end if;
 R_Typ : Node_Id) return Boolean
 is
 L_Ndims : constant Nat := Number_Dimensions (L_Typ);
 R_Ndims : constant Nat := Number_Dimensions (R_Typ);
-L_Index : Node_Id;
+L_Index : Node_Id := Empty; -- init to ...
-R_Index : Node_Id;
+R_Index : Node_Id := Empty; -- ...avoid warnings
 L_Low   : Node_Id;
 L_High  : Node_Id;
 L_Len   : Uint;
 R_Low   : Node_Id;
 R_High  : Node_Id;
 else
 return False;
 end if;
 end Needs_One_Actual;
+---------------------------------
+-- Needs_Simple_Initialization --
+---------------------------------
+function Needs_Simple_Initialization
+(Typ         : Entity_Id;
+Consider_IS : Boolean := True) return Boolean
+is
+Consider_IS_NS : constant Boolean :=
+Normalize_Scalars or (Initialize_Scalars and Consider_IS);
+begin
+--  Never need initialization if it is suppressed
+if Initialization_Suppressed (Typ) then
+return False;
+end if;
+--  Check for private type, in which case test applies to the underlying
+--  type of the private type.
+if Is_Private_Type (Typ) then
+declare
+RT : constant Entity_Id := Underlying_Type (Typ);
+begin
+if Present (RT) then
+return Needs_Simple_Initialization (RT);
+else
+return False;
+end if;
+end;
+--  Scalar type with Default_Value aspect requires initialization
+elsif Is_Scalar_Type (Typ) and then Has_Default_Aspect (Typ) then
+return True;
+--  Cases needing simple initialization are access types, and, if pragma
+--  Normalize_Scalars or Initialize_Scalars is in effect, then all scalar
+--  types.
+elsif Is_Access_Type (Typ)
+or else (Consider_IS_NS and then (Is_Scalar_Type (Typ)))
+then
+return True;
+--  If Initialize/Normalize_Scalars is in effect, string objects also
+--  need initialization, unless they are created in the course of
+--  expanding an aggregate (since in the latter case they will be
+--  filled with appropriate initializing values before they are used).
+elsif Consider_IS_NS
+and then Is_Standard_String_Type (Typ)
+and then
+(not Is_Itype (Typ)
+or else Nkind (Associated_Node_For_Itype (Typ)) /= N_Aggregate)
+then
+return True;
+else
+return False;
+end if;
+end Needs_Simple_Initialization;
+-------------------------------------
+-- Needs_Variable_Reference_Marker --
+-------------------------------------
+function Needs_Variable_Reference_Marker
+(N        : Node_Id;
+Calls_OK : Boolean) return Boolean
+is
+function Within_Suitable_Context (Ref : Node_Id) return Boolean;
+--  Deteremine whether variable reference Ref appears within a suitable
+--  context that allows the creation of a marker.
+-----------------------------
+-- Within_Suitable_Context --
+-----------------------------
+function Within_Suitable_Context (Ref : Node_Id) return Boolean is
+Par : Node_Id;
+begin
+Par := Ref;
+while Present (Par) loop
+--  The context is not suitable when the reference appears within
+--  the formal part of an instantiation which acts as compilation
+--  unit because there is no proper list for the insertion of the
+--  marker.
+if Nkind (Par) = N_Generic_Association
+and then Nkind (Parent (Par)) in N_Generic_Instantiation
+and then Nkind (Parent (Parent (Par))) = N_Compilation_Unit
+then
+return False;
+--  The context is not suitable when the reference appears within
+--  a pragma. If the pragma has run-time semantics, the reference
+--  will be reconsidered once the pragma is expanded.
+elsif Nkind (Par) = N_Pragma then
+return False;
+--  The context is not suitable when the reference appears within a
+--  subprogram call, and the caller requests this behavior.
+elsif not Calls_OK
+and then Nkind_In (Par, N_Entry_Call_Statement,
+N_Function_Call,
+N_Procedure_Call_Statement)
+then
+return False;
+--  Prevent the search from going too far
+elsif Is_Body_Or_Package_Declaration (Par) then
+exit;
+end if;
+Par := Parent (Par);
+end loop;
+return True;
+end Within_Suitable_Context;
+--  Local variables
+Prag   : Node_Id;
+Var_Id : Entity_Id;
+--  Start of processing for Needs_Variable_Reference_Marker
+begin
+--  No marker needs to be created when switch -gnatH (legacy elaboration
+--  checking mode enabled) is in effect because the legacy ABE mechanism
+--  does not use markers.
+if Legacy_Elaboration_Checks then
+return False;
+--  No marker needs to be created for ASIS because ABE diagnostics and
+--  checks are not performed in this mode.
+elsif ASIS_Mode then
+return False;
+--  No marker needs to be created when the reference is preanalyzed
+--  because the marker will be inserted in the wrong place.
+elsif Preanalysis_Active then
+return False;
+--  Only references warrant a marker
+elsif not Nkind_In (N, N_Expanded_Name, N_Identifier) then
+return False;
+--  Only source references warrant a marker
+elsif not Comes_From_Source (N) then
+return False;
+--  No marker needs to be created when the reference is erroneous, left
+--  in a bad state, or does not denote a variable.
+elsif not (Present (Entity (N))
+and then Ekind (Entity (N)) = E_Variable
+and then Entity (N) /= Any_Id)
+then
+return False;
+end if;
+Var_Id := Entity (N);
+Prag   := SPARK_Pragma (Var_Id);
+--  Both the variable and reference must appear in SPARK_Mode On regions
+--  because this elaboration scenario falls under the SPARK rules.
+if not (Comes_From_Source (Var_Id)
+and then Present (Prag)
+and then Get_SPARK_Mode_From_Annotation (Prag) = On
+and then Is_SPARK_Mode_On_Node (N))
+then
+return False;
+--  No marker needs to be created when the reference does not appear
+--  within a suitable context (see body for details).
+--  Performance note: parent traversal
+elsif not Within_Suitable_Context (N) then
+return False;
+end if;
+--  At this point it is known that the variable reference will play a
+--  role in ABE diagnostics and requires a marker.
+return True;
+end Needs_Variable_Reference_Marker;
 ------------------------
 -- New_Copy_List_Tree --
 ------------------------
 function New_Copy_List_Tree (List : List_Id) return List_Id is
 -------------------
 -- New_Copy_Tree --
 -------------------
 function New_Copy_Tree
-(Source    : Node_Id;
+(Source           : Node_Id;
-Map       : Elist_Id   := No_Elist;
+Map              : Elist_Id   := No_Elist;
-New_Sloc  : Source_Ptr := No_Location;
+New_Sloc         : Source_Ptr := No_Location;
-New_Scope : Entity_Id  := Empty) return Node_Id
+New_Scope        : Entity_Id  := Empty;
+Scopes_In_EWA_OK : Boolean    := False) return Node_Id
 is
 --  This routine performs low-level tree manipulations and needs access
 --  to the internals of the tree.
 use Atree.Unchecked_Access;
 procedure Update_Semantic_Fields (Id : Entity_Id) is
 begin
 --  Discriminant_Constraint
-if Has_Discriminants (Base_Type (Id)) then
+if Is_Type (Id) and then Has_Discriminants (Base_Type (Id)) then
 Set_Discriminant_Constraint (Id, Elist_Id (
 Copy_Field_With_Replacement
 (Field    => Union_Id (Discriminant_Constraint (Id)),
 Semantic => True)));
 end if;
 Copy_Field_With_Replacement
 (Field    => Union_Id (Packed_Array_Impl_Type (Id)),
 Semantic => True)));
 end if;
 end if;
+--  Prev_Entity
+Set_Prev_Entity (Id, Node_Id (
+Copy_Field_With_Replacement
+(Field    => Union_Id (Prev_Entity (Id)),
+Semantic => True)));
 --  Next_Entity
 Set_Next_Entity (Id, Node_Id (
 Copy_Field_With_Replacement
 begin
 pragma Assert (Nkind (Id) in N_Entity);
 pragma Assert (not Is_Itype (Id));
---  Nothing to do if the entity is not defined in the Actions list of
+--  Nothing to do when the entity is not defined in the Actions list
---  an N_Expression_With_Actions node.
+--  of an N_Expression_With_Actions node.
 if EWA_Level = 0 then
 return;
---  Nothing to do if the entity is defined within a scoping construct
+--  Nothing to do when the entity is defined in a scoping construct
---  of an N_Expression_With_Actions node.
+--  within an N_Expression_With_Actions node, unless the caller has
+--  requested their replication.
-elsif EWA_Inner_Scope_Level > 0 then
+--  ??? should this restriction be eliminated?
+elsif EWA_Inner_Scope_Level > 0 and then not Scopes_In_EWA_OK then
 return;
---  Nothing to do if the entity is not an object or a type. Relaxing
+--  Nothing to do when the entity does not denote a construct that
+--  may appear within an N_Expression_With_Actions node. Relaxing
 --  this restriction leads to a performance penalty.
-elsif not Ekind_In (Id, E_Constant, E_Variable)
+--  ??? this list is flaky, and may hide dormant bugs
+elsif not Ekind_In (Id, E_Block,
+E_Constant,
+E_Label,
+E_Procedure,
+E_Variable)
 and then not Is_Type (Id)
 then
 return;
---  Nothing to do if the entity was already visited
+--  Nothing to do when the entity was already visited
 elsif NCT_Tables_In_Use
 and then Present (NCT_New_Entities.Get (Id))
 then
 return;
---  Nothing to do if the declaration node of the entity is not within
+--  Nothing to do when the declaration node of the entity is not in
 --  the subtree being replicated.
 elsif not In_Subtree
 (N    => Declaration_Node (Id),
 Root => Source)
 begin
 pragma Assert (Nkind (Id) in N_Entity);
 --  Discriminant_Constraint
-if Has_Discriminants (Base_Type (Id)) then
+if Is_Type (Id) and then Has_Discriminants (Base_Type (Id)) then
 Visit_Field
 (Field    => Union_Id (Discriminant_Constraint (Id)),
 Semantic => True);
 end if;
 (Kind         : Entity_Kind;
 Scope_Id     : Entity_Id;
 Sloc_Value   : Source_Ptr;
 Related_Id   : Entity_Id;
 Suffix       : Character;
-Suffix_Index : Nat := 0;
+Suffix_Index : Int := 0;
 Prefix       : Character := ' ') return Entity_Id
 is
 N : constant Entity_Id :=
 Make_Defining_Identifier (Sloc_Value,
 New_External_Name
 Id_Char    : Character) return Entity_Id
 is
 N : constant Entity_Id := Make_Temporary (Sloc_Value, Id_Char);
 begin
-Set_Ekind          (N, Kind);
+Set_Ekind       (N, Kind);
-Set_Is_Internal    (N, True);
+Set_Is_Internal (N, True);
-Append_Entity      (N, Scope_Id);
+Append_Entity   (N, Scope_Id);
 if Kind in Type_Kind then
 Init_Size_Align (N);
 end if;
 -----------------
 -- Next_Actual --
 -----------------
 function Next_Actual (Actual_Id : Node_Id) return Node_Id is
-N  : Node_Id;
+Par : constant Node_Id := Parent (Actual_Id);
+N   : Node_Id;
 begin
 --  If we are pointing at a positional parameter, it is a member of a
 --  node list (the list of parameters), and the next parameter is the
 --  next node on the list, unless we hit a parameter association, then
 if Nkind (N) = N_Parameter_Association then
 --  In case of a build-in-place call, the call will no longer be a
 --  call; it will have been rewritten.
-if Nkind_In (Parent (Actual_Id), N_Entry_Call_Statement,
+if Nkind_In (Par, N_Entry_Call_Statement,
 N_Function_Call,
 N_Procedure_Call_Statement)
 then
-return First_Named_Actual (Parent (Actual_Id));
+return First_Named_Actual (Par);
+--  In case of a call rewritten in GNATprove mode while "inlining
+--  for proof" go to the original call.
+elsif Nkind (Par) = N_Null_Statement then
+pragma Assert
+(GNATprove_Mode
+and then
+Nkind (Original_Node (Par)) in N_Subprogram_Call);
+return First_Named_Actual (Original_Node (Par));
 else
 return Empty;
 end if;
 else
 return N;
 else
 Kind := Name_Ignore;
 end if;
 end if;
+--  In CodePeer mode and GNATprove mode, we need to consider all
+--  assertions, unless they are disabled. Force Name_Check on
+--  ignored assertions.
+if Nam_In (Kind, Name_Ignore, Name_Off)
+and then (CodePeer_Mode or GNATprove_Mode)
+then
+Kind := Name_Check;
+end if;
 return Kind;
 end Policy_In_Effect;
 ----------------------------------
 -- Predicate_Tests_On_Arguments --
 --  prevents accidental clobbering of enabled attributes.
 if Has_Inheritable_Invariants (From_Typ)
 and then not Has_Inheritable_Invariants (Typ)
 then
-Set_Has_Inheritable_Invariants (Typ, True);
+Set_Has_Inheritable_Invariants (Typ);
 end if;
 if Has_Inherited_Invariants (From_Typ)
 and then not Has_Inherited_Invariants (Typ)
 then
-Set_Has_Inherited_Invariants (Typ, True);
+Set_Has_Inherited_Invariants (Typ);
 end if;
 if Has_Own_Invariants (From_Typ)
 and then not Has_Own_Invariants (Typ)
 then
-Set_Has_Own_Invariants (Typ, True);
+Set_Has_Own_Invariants (Typ);
 end if;
 if Present (Full_IP) and then No (Invariant_Procedure (Typ)) then
 Set_Invariant_Procedure (Typ, Full_IP);
 end if;
 Refs  : Elist_Id;
 begin
 --  The variable is a constituent of a single protected/task type. Such
 --  a variable acts as a component of the type and must appear within a
---  specific region (SPARK RM 9.3). Instead of recording the reference,
+--  specific region (SPARK RM 9(3)). Instead of recording the reference,
 --  verify its legality now.
 if Present (Encap) and then Is_Single_Concurrent_Object (Encap) then
 Check_Part_Of_Reference (Var_Id, Ref);
 else
 return False;
 end if;
 end References_Generic_Formal_Type;
--------------------
+-------------------------------
--- Remove_Entity --
+-- Remove_Entity_And_Homonym --
--------------------
+-------------------------------
-procedure Remove_Entity (Id : Entity_Id) is
+procedure Remove_Entity_And_Homonym (Id : Entity_Id) is
-Scop    : constant Entity_Id := Scope (Id);
+begin
-Prev_Id : Entity_Id;
+Remove_Entity (Id);
+Remove_Homonym (Id);
-begin
+end Remove_Entity_And_Homonym;
---  Remove the entity from the homonym chain. When the entity is the
---  head of the chain, associate the entry in the name table with its
---  homonym effectively making it the new head of the chain.
-if Current_Entity (Id) = Id then
-Set_Name_Entity_Id (Chars (Id), Homonym (Id));
---  Otherwise link the previous and next homonyms
-else
-Prev_Id := Current_Entity (Id);
-while Present (Prev_Id) and then Homonym (Prev_Id) /= Id loop
-Prev_Id := Homonym (Prev_Id);
-end loop;
-Set_Homonym (Prev_Id, Homonym (Id));
-end if;
---  Remove the entity from the scope entity chain. When the entity is
---  the head of the chain, set the next entity as the new head of the
---  chain.
-if First_Entity (Scop) = Id then
-Prev_Id := Empty;
-Set_First_Entity (Scop, Next_Entity (Id));
---  Otherwise the entity is either in the middle of the chain or it acts
---  as its tail. Traverse and link the previous and next entities.
-else
-Prev_Id := First_Entity (Scop);
-while Present (Prev_Id) and then Next_Entity (Prev_Id) /= Id loop
-Next_Entity (Prev_Id);
-end loop;
-Set_Next_Entity (Prev_Id, Next_Entity (Id));
-end if;
---  Handle the case where the entity acts as the tail of the scope entity
---  chain.
-if Last_Entity (Scop) = Id then
-Set_Last_Entity (Scop, Prev_Id);
-end if;
-end Remove_Entity;
 --------------------
 -- Remove_Homonym --
 --------------------
-procedure Remove_Homonym (E : Entity_Id) is
+procedure Remove_Homonym (Id : Entity_Id) is
-Prev  : Entity_Id := Empty;
+Hom  : Entity_Id;
-H     : Entity_Id;
+Prev : Entity_Id := Empty;
 begin
-if E = Current_Entity (E) then
+if Id = Current_Entity (Id) then
-if Present (Homonym (E)) then
+if Present (Homonym (Id)) then
-Set_Current_Entity (Homonym (E));
+Set_Current_Entity (Homonym (Id));
 else
-Set_Name_Entity_Id (Chars (E), Empty);
+Set_Name_Entity_Id (Chars (Id), Empty);
 end if;
 else
-H := Current_Entity (E);
+Hom := Current_Entity (Id);
-while Present (H) and then H /= E loop
+while Present (Hom) and then Hom /= Id loop
-Prev := H;
+Prev := Hom;
-H    := Homonym (H);
+Hom  := Homonym (Hom);
 end loop;
---  If E is not on the homonym chain, nothing to do
+--  If Id is not on the homonym chain, nothing to do
-if Present (H) then
+if Present (Hom) then
-Set_Homonym (Prev, Homonym (E));
+Set_Homonym (Prev, Homonym (Id));
 end if;
 end if;
 end Remove_Homonym;
 ------------------------------
 Formal : Entity_Id;
 --  Start of processing for Remove_Overloaded_Entity
 begin
---  Remove the entity from both the homonym and scope chains
+Remove_Entity_And_Homonym (Id);
-Remove_Entity (Id);
 --  The entity denotes a primitive subprogram. Remove it from the list of
 --  primitives of the associated controlling type.
 if Ekind_In (Id, E_Function, E_Procedure) and then Is_Primitive (Id) then
 -------------------------
 -- Scalar_Part_Present --
 -------------------------
-function Scalar_Part_Present (T : Entity_Id) return Boolean is
+function Scalar_Part_Present (Typ : Entity_Id) return Boolean is
-C : Entity_Id;
+Val_Typ : constant Entity_Id := Validated_View (Typ);
+Field   : Entity_Id;
-begin
-if Is_Scalar_Type (T) then
+begin
+if Is_Scalar_Type (Val_Typ) then
 return True;
-elsif Is_Array_Type (T) then
+elsif Is_Array_Type (Val_Typ) then
-return Scalar_Part_Present (Component_Type (T));
+return Scalar_Part_Present (Component_Type (Val_Typ));
-elsif Is_Record_Type (T) or else Has_Discriminants (T) then
+elsif Is_Record_Type (Val_Typ) then
-C := First_Component_Or_Discriminant (T);
+Field := First_Component_Or_Discriminant (Val_Typ);
-while Present (C) loop
+while Present (Field) loop
-if Scalar_Part_Present (Etype (C)) then
+if Scalar_Part_Present (Etype (Field)) then
 return True;
-else
-Next_Component_Or_Discriminant (C);
 end if;
+Next_Component_Or_Discriminant (Field);
 end loop;
 end if;
 return False;
 end Scalar_Part_Present;
 while Present (Curr) and then Curr /= Standard_Standard loop
 Curr := Scope (Curr);
 if Curr = Outer then
 return True;
+--  A selective accept body appears within a task type, but the
+--  enclosing subprogram is the procedure of the task body.
+elsif Ekind (Curr) = E_Task_Type
+and then Outer = Task_Body_Procedure (Curr)
+then
+return True;
+--  Ditto for the body of a protected operation
+elsif Is_Subprogram (Curr)
+and then Outer = Protected_Body_Subprogram (Curr)
+then
+return True;
+--  Outside of its scope, a synchronized type may just be private
+elsif Is_Private_Type (Curr)
+and then Present (Full_View (Curr))
+and then Is_Concurrent_Type (Full_View (Curr))
+then
+return Scope_Within (Full_View (Curr), Outer);
 end if;
 end loop;
 return False;
 end Scope_Within;
 if Is_Type (E)
 and then Is_Access_Subprogram_Type (Base_Type (E))
 and then Has_Foreign_Convention (E)
 then
+Set_Can_Use_Internal_Rep (E, False);
---  A pragma Convention in an instance may apply to the subtype
---  created for a formal, in which case we have already verified
---  that conventions of actual and formal match and there is nothing
---  to flag on the subtype.
-if In_Instance then
-null;
-else
-Set_Can_Use_Internal_Rep (E, False);
-end if;
 end if;
 --  If E is an object, including a component, and the type of E is an
 --  anonymous access type with no convention set, then also set the
 --  convention of the anonymous access type. We do not do this for
 end if;
 Set_Entity (N, Val);
 end Set_Entity_With_Checks;
+------------------------------
+-- Set_Invalid_Scalar_Value --
+------------------------------
+procedure Set_Invalid_Scalar_Value
+(Scal_Typ : Float_Scalar_Id;
+Value    : Ureal)
+is
+Slot : Ureal renames Invalid_Floats (Scal_Typ);
+begin
+--  Detect an attempt to set a different value for the same scalar type
+pragma Assert (Slot = No_Ureal);
+Slot := Value;
+end Set_Invalid_Scalar_Value;
+------------------------------
+-- Set_Invalid_Scalar_Value --
+------------------------------
+procedure Set_Invalid_Scalar_Value
+(Scal_Typ : Integer_Scalar_Id;
+Value    : Uint)
+is
+Slot : Uint renames Invalid_Integers (Scal_Typ);
+begin
+--  Detect an attempt to set a different value for the same scalar type
+pragma Assert (Slot = No_Uint);
+Slot := Value;
+end Set_Invalid_Scalar_Value;
 ------------------------
 -- Set_Name_Entity_Id --
 ------------------------
 procedure Set_Name_Entity_Id (Id : Name_Id; Val : Entity_Id) is
 ---------------------
 function Subprogram_Name (N : Node_Id) return String is
 Buf : Bounded_String;
 Ent : Node_Id := N;
+Nod : Node_Id;
 begin
 while Present (Ent) loop
 case Nkind (Ent) is
 when N_Subprogram_Body =>
 Ent := Defining_Unit_Name (Specification (Ent));
 exit;
-when N_Package_Body
+when N_Subprogram_Declaration =>
+Nod := Corresponding_Body (Ent);
+if Present (Nod) then
+Ent := Nod;
+else
+Ent := Defining_Unit_Name (Specification (Ent));
+end if;
+exit;
+when N_Subprogram_Instantiation
+| N_Package_Body
 | N_Package_Specification
-| N_Subprogram_Specification
 =>
 Ent := Defining_Unit_Name (Ent);
 exit;
+when N_Protected_Type_Declaration =>
+Ent := Corresponding_Body (Ent);
+exit;
 when N_Protected_Body
-| N_Protected_Type_Declaration
 | N_Task_Body
 =>
+Ent := Defining_Identifier (Ent);
 exit;
 when others =>
 null;
 end case;
 Ent := Parent (Ent);
 end loop;
 if No (Ent) then
-return "unknown subprogram";
+return "unknown subprogram:unknown file:0:0";
 end if;
 --  If the subprogram is a child unit, use its simple name to start the
 --  construction of the fully qualified name.
 if Nkind (Ent) = N_Defining_Program_Unit_Name then
-Append_Entity_Name (Buf, Defining_Identifier (Ent));
+Ent := Defining_Identifier (Ent);
-else
+end if;
-Append_Entity_Name (Buf, Ent);
-end if;
+Append_Entity_Name (Buf, Ent);
+--  Append homonym number if needed
+if Nkind (N) in N_Entity and then Has_Homonym (N) then
+declare
+H  : Entity_Id := Homonym (N);
+Nr : Nat := 1;
+begin
+while Present (H) loop
+if Scope (H) = Scope (N) then
+Nr := Nr + 1;
+end if;
+H := Homonym (H);
+end loop;
+if Nr > 1 then
+Append (Buf, '#');
+Append (Buf, Nr);
+end if;
+end;
+end if;
+--  Append source location of Ent to Buf so that the string will
+--  look like "subp:file:line:col".
+declare
+Loc : constant Source_Ptr := Sloc (Ent);
+begin
+Append (Buf, ':');
+Append (Buf, Reference_Name (Get_Source_File_Index (Loc)));
+Append (Buf, ':');
+Append (Buf, Nat (Get_Logical_Line_Number (Loc)));
+Append (Buf, ':');
+Append (Buf, Nat (Get_Column_Number (Loc)));
+end;
 return +Buf;
 end Subprogram_Name;
 -------------------------------
 --  Merge the entity chain of the source scope with that of the
 --  destination scope.
 if Present (Last_Entity (To)) then
-Set_Next_Entity (Last_Entity (To), Id);
+Link_Entities (Last_Entity (To), Id);
 else
 Set_First_Entity (To, Id);
 end if;
 Set_Last_Entity (To, Last_Entity (From));
 else
 return Expr;
 end if;
 end Unqual_Conv;
+--------------------
+-- Validated_View --
+--------------------
+function Validated_View (Typ : Entity_Id) return Entity_Id is
+Continue : Boolean;
+Val_Typ  : Entity_Id;
+begin
+Continue := True;
+Val_Typ  := Base_Type (Typ);
+--  Obtain the full view of the input type by stripping away concurrency,
+--  derivations, and privacy.
+while Continue loop
+Continue := False;
+if Is_Concurrent_Type (Val_Typ) then
+if Present (Corresponding_Record_Type (Val_Typ)) then
+Continue := True;
+Val_Typ  := Corresponding_Record_Type (Val_Typ);
+end if;
+elsif Is_Derived_Type (Val_Typ) then
+Continue := True;
+Val_Typ  := Etype (Val_Typ);
+elsif Is_Private_Type (Val_Typ) then
+if Present (Underlying_Full_View (Val_Typ)) then
+Continue := True;
+Val_Typ  := Underlying_Full_View (Val_Typ);
+elsif Present (Full_View (Val_Typ)) then
+Continue := True;
+Val_Typ  := Full_View (Val_Typ);
+end if;
+end if;
+end loop;
+return Val_Typ;
+end Validated_View;
 -----------------------
 -- Visible_Ancestors --
 -----------------------
 function Visible_Ancestors (Typ : Entity_Id) return Elist_Id is
 function Within_Scope (E : Entity_Id; S : Entity_Id) return Boolean is
 begin
 return Scope_Within_Or_Same (Scope (E), S);
 end Within_Scope;
+----------------------------
+-- Within_Subprogram_Call --
+----------------------------
+function Within_Subprogram_Call (N : Node_Id) return Boolean is
+Par : Node_Id;
+begin
+--  Climb the parent chain looking for a function or procedure call
+Par := N;
+while Present (Par) loop
+if Nkind_In (Par, N_Entry_Call_Statement,
+N_Function_Call,
+N_Procedure_Call_Statement)
+then
+return True;
+--  Prevent the search from going too far
+elsif Is_Body_Or_Package_Declaration (Par) then
+exit;
+end if;
+Par := Parent (Par);
+end loop;
+return False;
+end Within_Subprogram_Call;
 ----------------
 -- Wrong_Type --
 ----------------

Mercurial > hg > CbC > CbC_gcc

comparison gcc/ada/sem_util.adb @ 131:84e7813d76e9