OSDN Git Service

Merge remote-tracking branch 'gnu/gcc-4_7-branch' into rework
[pf3gnuchains/gcc-fork.git] / gcc / ada / sem_ch3.adb
index 0587b9a..4618a71 100644 (file)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2012, 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- --
@@ -23,7 +23,6 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-with Aspects;  use Aspects;
 with Atree;    use Atree;
 with Checks;   use Checks;
 with Debug;    use Debug;
@@ -57,6 +56,7 @@ with Sem_Ch6;  use Sem_Ch6;
 with Sem_Ch7;  use Sem_Ch7;
 with Sem_Ch8;  use Sem_Ch8;
 with Sem_Ch13; use Sem_Ch13;
+with Sem_Dim;  use Sem_Dim;
 with Sem_Disp; use Sem_Disp;
 with Sem_Dist; use Sem_Dist;
 with Sem_Elim; use Sem_Elim;
@@ -585,8 +585,7 @@ package body Sem_Ch3 is
    --  given kind of type (index constraint to an array type, for example).
 
    procedure Modular_Type_Declaration (T : Entity_Id; Def : Node_Id);
-   --  Create new modular type. Verify that modulus is in bounds and is
-   --  a power of two (implementation restriction).
+   --  Create new modular type. Verify that modulus is in bounds
 
    procedure New_Concatenation_Op (Typ : Entity_Id);
    --  Create an abbreviated declaration for an operator in order to
@@ -708,14 +707,14 @@ package body Sem_Ch3 is
      (Related_Nod : Node_Id;
       N           : Node_Id) return Entity_Id
    is
-      Loc                 : constant Source_Ptr := Sloc (Related_Nod);
       Anon_Type           : Entity_Id;
       Anon_Scope          : Entity_Id;
       Desig_Type          : Entity_Id;
-      Decl                : Entity_Id;
       Enclosing_Prot_Type : Entity_Id := Empty;
 
    begin
+      Check_SPARK_Restriction ("access type is not allowed", N);
+
       if Is_Entry (Current_Scope)
         and then Is_Task_Type (Etype (Scope (Current_Scope)))
       then
@@ -728,13 +727,33 @@ package body Sem_Ch3 is
 
       --  If the access definition is the return type of another access to
       --  function, scope is the current one, because it is the one of the
-      --  current type declaration.
+      --  current type declaration, except for the pathological case below.
 
       if Nkind_In (Related_Nod, N_Object_Declaration,
                                 N_Access_Function_Definition)
       then
          Anon_Scope := Current_Scope;
 
+         --  A pathological case: function returning access functions that
+         --  return access functions, etc. Each anonymous access type created
+         --  is in the enclosing scope of the outermost function.
+
+         declare
+            Par : Node_Id;
+
+         begin
+            Par := Related_Nod;
+            while Nkind_In (Par, N_Access_Function_Definition,
+                                 N_Access_Definition)
+            loop
+               Par := Parent (Par);
+            end loop;
+
+            if Nkind (Par) = N_Function_Specification then
+               Anon_Scope := Scope (Defining_Entity (Par));
+            end if;
+         end;
+
       --  For the anonymous function result case, retrieve the scope of the
       --  function specification's associated entity rather than using the
       --  current scope. The current scope will be the function itself if the
@@ -772,16 +791,22 @@ package body Sem_Ch3 is
             Anon_Scope := Scope (Defining_Entity (Related_Nod));
          end if;
 
-      else
-         --  For access formals, access components, and access discriminants,
-         --  the scope is that of the enclosing declaration,
+      --  For an access type definition, if the current scope is a child
+      --  unit it is the scope of the type.
 
+      elsif Is_Compilation_Unit (Current_Scope) then
+         Anon_Scope := Current_Scope;
+
+      --  For access formals, access components, and access discriminants, the
+      --  scope is that of the enclosing declaration,
+
+      else
          Anon_Scope := Scope (Current_Scope);
       end if;
 
       Anon_Type :=
         Create_Itype
-         (E_Anonymous_Access_Type, Related_Nod, Scope_Id => Anon_Scope);
+          (E_Anonymous_Access_Type, Related_Nod, Scope_Id => Anon_Scope);
 
       if All_Present (N)
         and then Ada_Version >= Ada_2005
@@ -793,6 +818,13 @@ package body Sem_Ch3 is
       --  the corresponding semantic routine
 
       if Present (Access_To_Subprogram_Definition (N)) then
+
+         --  Compiler runtime units are compiled in Ada 2005 mode when building
+         --  the runtime library but must also be compilable in Ada 95 mode
+         --  (when bootstrapping the compiler).
+
+         Check_Compiler_Unit (N);
+
          Access_Subprogram_Declaration
            (T_Name => Anon_Type,
             T_Def  => Access_To_Subprogram_Definition (N));
@@ -808,7 +840,7 @@ package body Sem_Ch3 is
          Set_Can_Use_Internal_Rep
            (Anon_Type, not Always_Compatible_Rep_On_Target);
 
-         --  If the anonymous access is associated with a protected operation
+         --  If the anonymous access is associated with a protected operation,
          --  create a reference to it after the enclosing protected definition
          --  because the itype will be used in the subsequent bodies.
 
@@ -876,7 +908,7 @@ package body Sem_Ch3 is
       --  proper Master for the created tasks.
 
       if Nkind (Related_Nod) = N_Object_Declaration
-         and then Expander_Active
+        and then Expander_Active
       then
          if Is_Interface (Desig_Type)
            and then Is_Limited_Record (Desig_Type)
@@ -888,28 +920,9 @@ package body Sem_Ch3 is
 
          elsif Has_Task (Desig_Type)
            and then Comes_From_Source (Related_Nod)
-           and then not Restriction_Active (No_Task_Hierarchy)
          then
-            if not Has_Master_Entity (Current_Scope) then
-               Decl :=
-                 Make_Object_Declaration (Loc,
-                   Defining_Identifier =>
-                     Make_Defining_Identifier (Loc, Name_uMaster),
-                   Constant_Present => True,
-                   Object_Definition =>
-                     New_Reference_To (RTE (RE_Master_Id), Loc),
-                   Expression =>
-                     Make_Explicit_Dereference (Loc,
-                       New_Reference_To (RTE (RE_Current_Master), Loc)));
-
-               Insert_Before (Related_Nod, Decl);
-               Analyze (Decl);
-
-               Set_Master_Id (Anon_Type, Defining_Identifier (Decl));
-               Set_Has_Master_Entity (Current_Scope);
-            else
-               Build_Master_Renaming (Related_Nod, Anon_Type);
-            end if;
+            Build_Master_Entity (Defining_Identifier (Related_Nod));
+            Build_Master_Renaming (Anon_Type);
          end if;
       end if;
 
@@ -1028,6 +1041,8 @@ package body Sem_Ch3 is
    --  Start of processing for Access_Subprogram_Declaration
 
    begin
+      Check_SPARK_Restriction ("access type is not allowed", T_Def);
+
       --  Associate the Itype node with the inner full-type declaration or
       --  subprogram spec or entry body. This is required to handle nested
       --  anonymous declarations. For example:
@@ -1172,6 +1187,22 @@ package body Sem_Ch3 is
 
          begin
             F := First (Formals);
+
+            --  In ASIS mode, the access_to_subprogram may be analyzed twice,
+            --  when it is part of an unconstrained type and subtype expansion
+            --  is disabled. To avoid back-end problems with shared profiles,
+            --  use previous subprogram type as the designated type.
+
+            if ASIS_Mode
+              and then Present (Scope (Defining_Identifier (F)))
+            then
+               Set_Etype                    (T_Name, T_Name);
+               Init_Size_Align              (T_Name);
+               Set_Directly_Designated_Type (T_Name,
+                 Scope (Defining_Identifier (F)));
+               return;
+            end if;
+
             while Present (F) loop
                if No (Parent (Defining_Identifier (F))) then
                   Set_Parent (Defining_Identifier (F), F);
@@ -1261,9 +1292,14 @@ package body Sem_Ch3 is
    ----------------------------
 
    procedure Access_Type_Declaration (T : Entity_Id; Def : Node_Id) is
-      S : constant Node_Id := Subtype_Indication (Def);
       P : constant Node_Id := Parent (Def);
+      S : constant Node_Id := Subtype_Indication (Def);
+
+      Full_Desig : Entity_Id;
+
    begin
+      Check_SPARK_Restriction ("access type is not allowed", Def);
+
       --  Check for permissible use of incomplete type
 
       if Nkind (S) /= N_Subtype_Indication then
@@ -1287,15 +1323,17 @@ package body Sem_Ch3 is
          Set_Ekind (T, E_Access_Type);
       end if;
 
-      if Base_Type (Designated_Type (T)) = T then
+      Full_Desig := Designated_Type (T);
+
+      if Base_Type (Full_Desig) = T then
          Error_Msg_N ("access type cannot designate itself", S);
 
       --  In Ada 2005, the type may have a limited view through some unit
       --  in its own context, allowing the following circularity that cannot
       --  be detected earlier
 
-      elsif Is_Class_Wide_Type (Designated_Type (T))
-        and then Etype (Designated_Type (T)) = T
+      elsif Is_Class_Wide_Type (Full_Desig)
+        and then Etype (Full_Desig) = T
       then
          Error_Msg_N
            ("access type cannot designate its own classwide type", S);
@@ -1321,12 +1359,19 @@ package body Sem_Ch3 is
       Set_Has_Task (T, False);
       Set_Has_Controlled_Component (T, False);
 
-      --  Initialize Associated_Final_Chain explicitly to Empty, to avoid
+      --  Initialize field Finalization_Master explicitly to Empty, to avoid
       --  problems where an incomplete view of this entity has been previously
       --  established by a limited with and an overlaid version of this field
       --  (Stored_Constraint) was initialized for the incomplete view.
 
-      Set_Associated_Final_Chain (T, Empty);
+      --  This reset is performed in most cases except where the access type
+      --  has been created for the purposes of allocating or deallocating a
+      --  build-in-place object. Such access types have explicitly set pools
+      --  and finalization masters.
+
+      if No (Associated_Storage_Pool (T)) then
+         Set_Finalization_Master (T, Empty);
+      end if;
 
       --  Ada 2005 (AI-231): Propagate the null-excluding and access-constant
       --  attributes
@@ -1570,6 +1615,10 @@ package body Sem_Ch3 is
                    (Tagged_Type => Tagged_Type,
                     Iface_Prim  => Iface_Prim);
 
+               if No (Prim) and then Serious_Errors_Detected > 0 then
+                  goto Continue;
+               end if;
+
                pragma Assert (Present (Prim));
 
                --  Ada 2012 (AI05-0197): If the name of the covering primitive
@@ -1630,6 +1679,7 @@ package body Sem_Ch3 is
                Set_Has_Delayed_Freeze (New_Subp);
             end if;
 
+            <<Continue>>
             Next_Elmt (Elmt);
          end loop;
 
@@ -1646,10 +1696,12 @@ package body Sem_Ch3 is
    -----------------------------------
 
    procedure Analyze_Component_Declaration (N : Node_Id) is
-      Id : constant Entity_Id := Defining_Identifier (N);
-      E  : constant Node_Id   := Expression (N);
-      T  : Entity_Id;
-      P  : Entity_Id;
+      Id  : constant Entity_Id := Defining_Identifier (N);
+      E   : constant Node_Id   := Expression (N);
+      Typ : constant Node_Id   :=
+              Subtype_Indication (Component_Definition (N));
+      T   : Entity_Id;
+      P   : Entity_Id;
 
       function Contains_POC (Constr : Node_Id) return Boolean;
       --  Determines whether a constraint uses the discriminant of a record
@@ -1759,10 +1811,14 @@ package body Sem_Ch3 is
       Generate_Definition (Id);
       Enter_Name (Id);
 
-      if Present (Subtype_Indication (Component_Definition (N))) then
+      if Present (Typ) then
          T := Find_Type_Of_Object
                 (Subtype_Indication (Component_Definition (N)), N);
 
+         if not Nkind_In (Typ, N_Identifier, N_Expanded_Name) then
+            Check_SPARK_Restriction ("subtype mark required", Typ);
+         end if;
+
       --  Ada 2005 (AI-230): Access Definition case
 
       else
@@ -1813,6 +1869,7 @@ package body Sem_Ch3 is
       --  package Sem).
 
       if Present (E) then
+         Check_SPARK_Restriction ("default expression is not allowed", E);
          Preanalyze_Spec_Expression (E, T);
          Check_Initialization (T, E);
 
@@ -1840,7 +1897,9 @@ package body Sem_Ch3 is
             --  (Ada 2005: AI-230): Accessibility check for anonymous
             --  components
 
-            if Type_Access_Level (Etype (E)) > Type_Access_Level (T) then
+            if Type_Access_Level (Etype (E)) >
+               Deepest_Type_Access_Level (T)
+            then
                Error_Msg_N
                  ("expression has deeper access level than component " &
                   "(RM 3.10.2 (12.2))", E);
@@ -1974,7 +2033,12 @@ package body Sem_Ch3 is
       end if;
 
       Set_Original_Record_Component (Id, Id);
-      Analyze_Aspect_Specifications (N, Id, Aspect_Specifications (N));
+
+      if Has_Aspects (N) then
+         Analyze_Aspect_Specifications (N, Id);
+      end if;
+
+      Analyze_Dimension (N);
    end Analyze_Component_Declaration;
 
    --------------------------
@@ -2008,9 +2072,23 @@ package body Sem_Ch3 is
    --  Start of processing for Analyze_Declarations
 
    begin
+      if Restriction_Check_Required (SPARK) then
+         Check_Later_Vs_Basic_Declarations (L, During_Parsing => False);
+      end if;
+
       D := First (L);
       while Present (D) loop
 
+         --  Package spec cannot contain a package declaration in SPARK
+
+         if Nkind (D) = N_Package_Declaration
+           and then Nkind (Parent (L)) = N_Package_Specification
+         then
+            Check_SPARK_Restriction
+              ("package specification cannot contain a package declaration",
+               D);
+         end if;
+
          --  Complete analysis of declaration
 
          Analyze (D);
@@ -2117,11 +2195,20 @@ package body Sem_Ch3 is
             if Nkind (Original_Node (Decl)) = N_Subprogram_Declaration then
                Spec := Specification (Original_Node (Decl));
                Sent := Defining_Unit_Name (Spec);
-               Prag := Spec_PPC_List (Sent);
+
+               Prag := Spec_PPC_List (Contract (Sent));
                while Present (Prag) loop
                   Analyze_PPC_In_Decl_Part (Prag, Sent);
                   Prag := Next_Pragma (Prag);
                end loop;
+
+               Check_Subprogram_Contract (Sent);
+
+               Prag := Spec_TC_List (Contract (Sent));
+               while Present (Prag) loop
+                  Analyze_TC_In_Decl_Part (Prag, Sent);
+                  Prag := Next_Pragma (Prag);
+               end loop;
             end if;
 
             Next (Decl);
@@ -2146,9 +2233,12 @@ package body Sem_Ch3 is
                                     or else In_Package_Body (Current_Scope));
 
       procedure Check_Ops_From_Incomplete_Type;
-      --  If there is a tagged incomplete partial view of the type, transfer
-      --  its operations to the full view, and indicate that the type of the
-      --  controlling parameter (s) is this full view.
+      --  If there is a tagged incomplete partial view of the type, traverse
+      --  the primitives of the incomplete view and change the type of any
+      --  controlling formals and result to indicate the full view. The
+      --  primitives will be added to the full type's primitive operations
+      --  list later in Sem_Disp.Check_Operation_From_Incomplete_Type (which
+      --  is called from Process_Incomplete_Dependents).
 
       ------------------------------------
       -- Check_Ops_From_Incomplete_Type --
@@ -2168,7 +2258,6 @@ package body Sem_Ch3 is
             Elmt := First_Elmt (Primitive_Operations (Prev));
             while Present (Elmt) loop
                Op := Node (Elmt);
-               Prepend_Elmt (Op, Primitive_Operations (T));
 
                Formal := First_Formal (Op);
                while Present (Formal) loop
@@ -2226,17 +2315,23 @@ package body Sem_Ch3 is
          when N_Derived_Type_Definition =>
             null;
 
-         --  For record types, discriminants are allowed
+         --  For record types, discriminants are allowed, unless we are in
+         --  SPARK.
 
          when N_Record_Definition =>
-            null;
+            if Present (Discriminant_Specifications (N)) then
+               Check_SPARK_Restriction
+                 ("discriminant type is not allowed",
+                  Defining_Identifier
+                    (First (Discriminant_Specifications (N))));
+            end if;
 
          when others =>
             if Present (Discriminant_Specifications (N)) then
                Error_Msg_N
                  ("elementary or array type cannot have discriminants",
                   Defining_Identifier
-                  (First (Discriminant_Specifications (N))));
+                    (First (Discriminant_Specifications (N))));
             end if;
       end case;
 
@@ -2331,6 +2426,12 @@ package body Sem_Ch3 is
          return;
       end if;
 
+      --  Controlled type is not allowed in SPARK
+
+      if Is_Visibly_Controlled (T) then
+         Check_SPARK_Restriction ("controlled type is not allowed", N);
+      end if;
+
       --  Some common processing for all types
 
       Set_Depends_On_Private (T, Has_Private_Component (T));
@@ -2423,7 +2524,17 @@ package body Sem_Ch3 is
       Set_Optimize_Alignment_Flags (Def_Id);
       Check_Eliminated (Def_Id);
 
-      Analyze_Aspect_Specifications (N, Def_Id, Aspect_Specifications (N));
+      --  If the declaration is a completion and aspects are present, apply
+      --  them to the entity for the type which is currently the partial
+      --  view, but which is the one that will be frozen.
+
+      if Has_Aspects (N) then
+         if Prev /= Def_Id then
+            Analyze_Aspect_Specifications (N, Prev);
+         else
+            Analyze_Aspect_Specifications (N, Def_Id);
+         end if;
+      end if;
    end Analyze_Full_Type_Declaration;
 
    ----------------------------------
@@ -2435,6 +2546,8 @@ package body Sem_Ch3 is
       T : Entity_Id;
 
    begin
+      Check_SPARK_Restriction ("incomplete type is not allowed", N);
+
       Generate_Definition (Defining_Identifier (N));
 
       --  Process an incomplete declaration. The identifier must not have been
@@ -2475,7 +2588,7 @@ package body Sem_Ch3 is
       --  subtypes will be built after the full view of the type.
 
       Set_Private_Dependents (T, New_Elmt_List);
-      Set_Is_Pure (T, F);
+      Set_Is_Pure            (T, F);
    end Analyze_Incomplete_Type_Decl;
 
    -----------------------------------
@@ -2576,8 +2689,8 @@ package body Sem_Ch3 is
       --  Process expression, replacing error by integer zero, to avoid
       --  cascaded errors or aborts further along in the processing
 
-      --  Replace Error by integer zero, which seems least likely to
-      --  cause cascaded errors.
+      --  Replace Error by integer zero, which seems least likely to cause
+      --  cascaded errors.
 
       if E = Error then
          Rewrite (E, Make_Integer_Literal (Sloc (E), Uint_0));
@@ -2763,12 +2876,12 @@ package body Sem_Ch3 is
       --  There are three kinds of implicit types generated by an
       --  object declaration:
 
-      --   1. Those for generated by the original Object Definition
+      --   1. Those generated by the original Object Definition
 
       --   2. Those generated by the Expression
 
-      --   3. Those used to constrained the Object Definition with the
-      --       expression constraints when it is unconstrained
+      --   3. Those used to constrain the Object Definition with the
+      --      expression constraints when the definition is unconstrained.
 
       --  They must be generated in this order to avoid order of elaboration
       --  issues. Thus the first step (after entering the name) is to analyze
@@ -2779,6 +2892,7 @@ package body Sem_Ch3 is
 
          if Present (Prev_Entity)
            and then
+
              --  If the homograph is an implicit subprogram, it is overridden
              --  by the current declaration.
 
@@ -2879,6 +2993,8 @@ package body Sem_Ch3 is
          end if;
       end if;
 
+      --  Object is marked pure if it is in a pure scope
+
       Set_Is_Pure (Id, Is_Pure (Current_Scope));
 
       --  If deferred constant, make sure context is appropriate. We detect
@@ -2968,6 +3084,35 @@ package body Sem_Ch3 is
 
       Act_T := T;
 
+      --  These checks should be performed before the initialization expression
+      --  is considered, so that the Object_Definition node is still the same
+      --  as in source code.
+
+      --  In SPARK, the nominal subtype shall be given by a subtype mark and
+      --  shall not be unconstrained. (The only exception to this is the
+      --  admission of declarations of constants of type String.)
+
+      if not
+        Nkind_In (Object_Definition (N), N_Identifier, N_Expanded_Name)
+      then
+         Check_SPARK_Restriction
+           ("subtype mark required", Object_Definition (N));
+
+      elsif Is_Array_Type (T)
+        and then not Is_Constrained (T)
+        and then T /= Standard_String
+      then
+         Check_SPARK_Restriction
+           ("subtype mark of constrained type expected",
+            Object_Definition (N));
+      end if;
+
+      --  There are no aliased objects in SPARK
+
+      if Aliased_Present (N) then
+         Check_SPARK_Restriction ("aliased object is not allowed", N);
+      end if;
+
       --  Process initialization expression if present and not in error
 
       if Present (E) and then E /= Error then
@@ -2982,8 +3127,8 @@ package body Sem_Ch3 is
              (Is_CPP_Class (Root_Type (Etype (Act_T)))
                or else
                  (Present (Full_View (Root_Type (Etype (Act_T))))
-                    and then
-                      Is_CPP_Class (Full_View (Root_Type (Etype (Act_T))))))
+                   and then
+                     Is_CPP_Class (Full_View (Root_Type (Etype (Act_T))))))
          then
             Error_Msg_N
               ("predefined assignment not available for 'C'P'P tagged types",
@@ -3083,6 +3228,18 @@ package body Sem_Ch3 is
 
          Apply_Scalar_Range_Check (E, T);
          Apply_Static_Length_Check (E, T);
+
+         if Nkind (Original_Node (N)) = N_Object_Declaration
+           and then Comes_From_Source (Original_Node (N))
+
+           --  Only call test if needed
+
+           and then Restriction_Check_Required (SPARK)
+           and then not Is_SPARK_Initialization_Expr (E)
+         then
+            Check_SPARK_Restriction
+              ("initialization expression is not appropriate", E);
+         end if;
       end if;
 
       --  If the No_Streams restriction is set, check that the type of the
@@ -3122,6 +3279,15 @@ package body Sem_Ch3 is
 
       if Is_Indefinite_Subtype (T) then
 
+         --  In SPARK, a declaration of unconstrained type is allowed
+         --  only for constants of type string.
+
+         if Is_String_Type (T) and then not Constant_Present (N) then
+            Check_SPARK_Restriction
+              ("declaration of object of unconstrained type not allowed",
+               N);
+         end if;
+
          --  Nothing to do in deferred constant case
 
          if Constant_Present (N) and then No (E) then
@@ -3168,9 +3334,12 @@ package body Sem_Ch3 is
          --  Case of initialization present
 
          else
-            --  Not allowed in Ada 83
+            --  Check restrictions in Ada 83
 
             if not Constant_Present (N) then
+
+               --  Unconstrained variables not allowed in Ada 83 mode
+
                if Ada_Version = Ada_83
                  and then Comes_From_Source (Object_Definition (N))
                then
@@ -3289,15 +3458,27 @@ package body Sem_Ch3 is
          --  It is unclear why this should make it acceptable to gcc. ???
 
          Remove_Side_Effects (E);
+
+      --  If this is a constant declaration of an unconstrained type and
+      --  the initialization is an aggregate, we can use the subtype of the
+      --  aggregate for the declared entity because it is immutable.
+
+      elsif not Is_Constrained (T)
+        and then Has_Discriminants (T)
+        and then Constant_Present (N)
+        and then not Has_Unchecked_Union (T)
+        and then Nkind (E) = N_Aggregate
+      then
+         Act_T := Etype (E);
       end if;
 
       --  Check No_Wide_Characters restriction
 
       Check_Wide_Character_Restriction (T, Object_Definition (N));
 
-      --  Indicate this is not set in source. Certainly true for constants,
-      --  and true for variables so far (will be reset for a variable if and
-      --  when we encounter a modification in the source).
+      --  Indicate this is not set in source. Certainly true for constants, and
+      --  true for variables so far (will be reset for a variable if and when
+      --  we encounter a modification in the source).
 
       Set_Never_Set_In_Source (Id, True);
 
@@ -3311,9 +3492,9 @@ package body Sem_Ch3 is
          Set_Ekind (Id, E_Variable);
 
          --  A variable is set as shared passive if it appears in a shared
-         --  passive package, and is at the outer level. This is not done
-         --  for entities generated during expansion, because those are
-         --  always manipulated locally.
+         --  passive package, and is at the outer level. This is not done for
+         --  entities generated during expansion, because those are always
+         --  manipulated locally.
 
          if Is_Shared_Passive (Current_Scope)
            and then Is_Library_Level_Entity (Id)
@@ -3368,6 +3549,14 @@ package body Sem_Ch3 is
 
       Set_Etype (Id, Act_T);
 
+      --  Object is marked to be treated as volatile if type is volatile and
+      --  we clear the Current_Value setting that may have been set above.
+
+      if Treat_As_Volatile (Etype (Id)) then
+         Set_Treat_As_Volatile (Id);
+         Set_Current_Value (Id, Empty);
+      end if;
+
       --  Deal with controlled types
 
       if Has_Controlled_Component (Etype (Id))
@@ -3586,14 +3775,19 @@ package body Sem_Ch3 is
 
       --  Check for violation of No_Local_Timing_Events
 
-      if Is_RTE (Etype (Id), RE_Timing_Event)
+      if Restriction_Check_Required (No_Local_Timing_Events)
         and then not Is_Library_Level_Entity (Id)
+        and then Is_RTE (Etype (Id), RE_Timing_Event)
       then
          Check_Restriction (No_Local_Timing_Events, N);
       end if;
 
-      <<Leave>>
-         Analyze_Aspect_Specifications (N, Id, Aspect_Specifications (N));
+   <<Leave>>
+      if Has_Aspects (N) then
+         Analyze_Aspect_Specifications (N, Id);
+      end if;
+
+      Analyze_Dimension (N);
    end Analyze_Object_Declaration;
 
    ---------------------------
@@ -3832,8 +4026,10 @@ package body Sem_Ch3 is
          end if;
       end if;
 
-      <<Leave>>
-         Analyze_Aspect_Specifications (N, T, Aspect_Specifications (N));
+   <<Leave>>
+      if Has_Aspects (N) then
+         Analyze_Aspect_Specifications (N, T);
+      end if;
    end Analyze_Private_Extension_Declaration;
 
    ---------------------------------
@@ -3871,9 +4067,9 @@ package body Sem_Ch3 is
 
       if Skip
         or else (Present (Etype (Id))
-                   and then (Is_Private_Type (Etype (Id))
-                               or else Is_Task_Type (Etype (Id))
-                               or else Is_Rewrite_Substitution (N)))
+                  and then (Is_Private_Type (Etype (Id))
+                             or else Is_Task_Type (Etype (Id))
+                             or else Is_Rewrite_Substitution (N)))
       then
          null;
 
@@ -3883,6 +4079,19 @@ package body Sem_Ch3 is
 
       T := Process_Subtype (Subtype_Indication (N), N, Id, 'P');
 
+      --  Class-wide equivalent types of records with unknown discriminants
+      --  involve the generation of an itype which serves as the private view
+      --  of a constrained record subtype. In such cases the base type of the
+      --  current subtype we are processing is the private itype. Use the full
+      --  of the private itype when decorating various attributes.
+
+      if Is_Itype (T)
+        and then Is_Private_Type (T)
+        and then Present (Full_View (T))
+      then
+         T := Full_View (T);
+      end if;
+
       --  Inherit common attributes
 
       Set_Is_Generic_Type   (Id, Is_Generic_Type   (Base_Type (T)));
@@ -3901,12 +4110,64 @@ package body Sem_Ch3 is
 
       if Has_Predicates (T)
         or else (Present (Ancestor_Subtype (T))
-                   and then Has_Predicates (Ancestor_Subtype (T)))
+                  and then Has_Predicates (Ancestor_Subtype (T)))
       then
          Set_Has_Predicates (Id);
          Set_Has_Delayed_Freeze (Id);
       end if;
 
+      --  Subtype of Boolean cannot have a constraint in SPARK
+
+      if Is_Boolean_Type (T)
+        and then Nkind (Subtype_Indication (N)) = N_Subtype_Indication
+      then
+         Check_SPARK_Restriction
+           ("subtype of Boolean cannot have constraint", N);
+      end if;
+
+      if Nkind (Subtype_Indication (N)) = N_Subtype_Indication then
+         declare
+            Cstr     : constant Node_Id := Constraint (Subtype_Indication (N));
+            One_Cstr : Node_Id;
+            Low      : Node_Id;
+            High     : Node_Id;
+
+         begin
+            if Nkind (Cstr) = N_Index_Or_Discriminant_Constraint then
+               One_Cstr := First (Constraints (Cstr));
+               while Present (One_Cstr) loop
+
+                  --  Index or discriminant constraint in SPARK must be a
+                  --  subtype mark.
+
+                  if not
+                    Nkind_In (One_Cstr, N_Identifier, N_Expanded_Name)
+                  then
+                     Check_SPARK_Restriction
+                       ("subtype mark required", One_Cstr);
+
+                  --  String subtype must have a lower bound of 1 in SPARK.
+                  --  Note that we do not need to test for the non-static case
+                  --  here, since that was already taken care of in
+                  --  Process_Range_Expr_In_Decl.
+
+                  elsif Base_Type (T) = Standard_String then
+                     Get_Index_Bounds (One_Cstr, Low, High);
+
+                     if Is_OK_Static_Expression (Low)
+                       and then Expr_Value (Low) /= 1
+                     then
+                        Check_SPARK_Restriction
+                          ("String subtype must have lower bound of 1", N);
+                     end if;
+                  end if;
+
+                  Next (One_Cstr);
+               end loop;
+            end if;
+         end;
+      end if;
+
       --  In the case where there is no constraint given in the subtype
       --  indication, Process_Subtype just returns the Subtype_Mark, so its
       --  semantic attributes must be established here.
@@ -3914,6 +4175,16 @@ package body Sem_Ch3 is
       if Nkind (Subtype_Indication (N)) /= N_Subtype_Indication then
          Set_Etype (Id, Base_Type (T));
 
+         --  Subtype of unconstrained array without constraint is not allowed
+         --  in SPARK.
+
+         if Is_Array_Type (T)
+           and then not Is_Constrained (T)
+         then
+            Check_SPARK_Restriction
+              ("subtype of unconstrained array must have constraint", N);
+         end if;
+
          case Ekind (T) is
             when Array_Kind =>
                Set_Ekind                       (Id, E_Array_Subtype);
@@ -3999,6 +4270,8 @@ package body Sem_Ch3 is
                Set_Has_Discriminants    (Id, Has_Discriminants  (T));
                Set_Is_Constrained       (Id, Is_Constrained     (T));
                Set_Is_Limited_Record    (Id, Is_Limited_Record  (T));
+               Set_Has_Implicit_Dereference
+                                        (Id, Has_Implicit_Dereference (T));
                Set_Has_Unknown_Discriminants
                                         (Id, Has_Unknown_Discriminants (T));
 
@@ -4025,22 +4298,24 @@ package body Sem_Ch3 is
                end if;
 
             when Private_Kind =>
-               Set_Ekind              (Id, Subtype_Kind (Ekind   (T)));
-               Set_Has_Discriminants  (Id, Has_Discriminants     (T));
-               Set_Is_Constrained     (Id, Is_Constrained        (T));
-               Set_First_Entity       (Id, First_Entity          (T));
-               Set_Last_Entity        (Id, Last_Entity           (T));
+               Set_Ekind              (Id, Subtype_Kind (Ekind        (T)));
+               Set_Has_Discriminants  (Id, Has_Discriminants          (T));
+               Set_Is_Constrained     (Id, Is_Constrained             (T));
+               Set_First_Entity       (Id, First_Entity               (T));
+               Set_Last_Entity        (Id, Last_Entity                (T));
                Set_Private_Dependents (Id, New_Elmt_List);
-               Set_Is_Limited_Record  (Id, Is_Limited_Record     (T));
+               Set_Is_Limited_Record  (Id, Is_Limited_Record          (T));
+               Set_Has_Implicit_Dereference
+                                      (Id, Has_Implicit_Dereference   (T));
                Set_Has_Unknown_Discriminants
-                                      (Id, Has_Unknown_Discriminants (T));
+                                      (Id, Has_Unknown_Discriminants  (T));
                Set_Known_To_Have_Preelab_Init
                                       (Id, Known_To_Have_Preelab_Init (T));
 
                if Is_Tagged_Type (T) then
                   Set_Is_Tagged_Type              (Id);
                   Set_Is_Abstract_Type            (Id, Is_Abstract_Type (T));
-                  Set_Class_Wide_Type             (Id, Class_Wide_Type (T));
+                  Set_Class_Wide_Type             (Id, Class_Wide_Type  (T));
                   Set_Direct_Primitive_Operations (Id,
                     Direct_Primitive_Operations (T));
                end if;
@@ -4053,14 +4328,14 @@ package body Sem_Ch3 is
 
                if Has_Discriminants (T) then
                   Set_Discriminant_Constraint
-                                     (Id, Discriminant_Constraint (T));
+                    (Id, Discriminant_Constraint (T));
                   Set_Stored_Constraint_From_Discriminant_Constraint (Id);
 
                elsif Present (Full_View (T))
                  and then Has_Discriminants (Full_View (T))
                then
                   Set_Discriminant_Constraint
-                               (Id, Discriminant_Constraint (Full_View (T)));
+                    (Id, Discriminant_Constraint (Full_View (T)));
                   Set_Stored_Constraint_From_Discriminant_Constraint (Id);
 
                   --  This would seem semantically correct, but apparently
@@ -4210,9 +4485,9 @@ package body Sem_Ch3 is
          Conditional_Delay (Id, T);
       end if;
 
-      --  Check that constraint_error is raised for a scalar subtype
-      --  indication when the lower or upper bound of a non-null range
-      --  lies outside the range of the type mark.
+      --  Check that Constraint_Error is raised for a scalar subtype indication
+      --  when the lower or upper bound of a non-null range lies outside the
+      --  range of the type mark.
 
       if Nkind (Subtype_Indication (N)) = N_Subtype_Indication then
          if Is_Scalar_Type (Etype (Id))
@@ -4224,38 +4499,69 @@ package body Sem_Ch3 is
               (Scalar_Range (Id),
                Etype (Subtype_Mark (Subtype_Indication (N))));
 
+         --  In the array case, check compatibility for each index
+
          elsif Is_Array_Type (Etype (Id))
            and then Present (First_Index (Id))
          then
             --  This really should be a subprogram that finds the indications
             --  to check???
 
-            if ((Nkind (First_Index (Id)) = N_Identifier
-                   and then Ekind (Entity (First_Index (Id))) in Scalar_Kind)
-                 or else Nkind (First_Index (Id)) = N_Subtype_Indication)
-              and then
-                Nkind (Scalar_Range (Etype (First_Index (Id)))) = N_Range
-            then
-               declare
-                  Target_Typ : constant Entity_Id :=
-                                 Etype
-                                   (First_Index (Etype
-                                     (Subtype_Mark (Subtype_Indication (N)))));
-               begin
-                  R_Checks :=
-                    Get_Range_Checks
-                      (Scalar_Range (Etype (First_Index (Id))),
-                       Target_Typ,
-                       Etype (First_Index (Id)),
-                       Defining_Identifier (N));
-
-                  Insert_Range_Checks
-                    (R_Checks,
-                     N,
-                     Target_Typ,
-                     Sloc (Defining_Identifier (N)));
-               end;
-            end if;
+            declare
+               Subt_Index   : Node_Id := First_Index (Id);
+               Target_Index : Node_Id :=
+                                First_Index (Etype
+                                  (Subtype_Mark (Subtype_Indication (N))));
+               Has_Dyn_Chk  : Boolean := Has_Dynamic_Range_Check (N);
+
+            begin
+               while Present (Subt_Index) loop
+                  if ((Nkind (Subt_Index) = N_Identifier
+                         and then Ekind (Entity (Subt_Index)) in Scalar_Kind)
+                       or else Nkind (Subt_Index) = N_Subtype_Indication)
+                    and then
+                      Nkind (Scalar_Range (Etype (Subt_Index))) = N_Range
+                  then
+                     declare
+                        Target_Typ : constant Entity_Id :=
+                                       Etype (Target_Index);
+                     begin
+                        R_Checks :=
+                          Get_Range_Checks
+                            (Scalar_Range (Etype (Subt_Index)),
+                             Target_Typ,
+                             Etype (Subt_Index),
+                             Defining_Identifier (N));
+
+                        --  Reset Has_Dynamic_Range_Check on the subtype to
+                        --  prevent elision of the index check due to a dynamic
+                        --  check generated for a preceding index (needed since
+                        --  Insert_Range_Checks tries to avoid generating
+                        --  redundant checks on a given declaration).
+
+                        Set_Has_Dynamic_Range_Check (N, False);
+
+                        Insert_Range_Checks
+                          (R_Checks,
+                           N,
+                           Target_Typ,
+                           Sloc (Defining_Identifier (N)));
+
+                        --  Record whether this index involved a dynamic check
+
+                        Has_Dyn_Chk :=
+                          Has_Dyn_Chk or else Has_Dynamic_Range_Check (N);
+                     end;
+                  end if;
+
+                  Next_Index (Subt_Index);
+                  Next_Index (Target_Index);
+               end loop;
+
+               --  Finally, mark whether the subtype involves dynamic checks
+
+               Set_Has_Dynamic_Range_Check (N, Has_Dyn_Chk);
+            end;
          end if;
       end if;
 
@@ -4277,7 +4583,11 @@ package body Sem_Ch3 is
       Check_Eliminated (Id);
 
    <<Leave>>
-      Analyze_Aspect_Specifications (N, Id, Aspect_Specifications (N));
+      if Has_Aspects (N) then
+         Analyze_Aspect_Specifications (N, Id);
+      end if;
+
+      Analyze_Dimension (N);
    end Analyze_Subtype_Declaration;
 
    --------------------------------
@@ -4400,6 +4710,7 @@ package body Sem_Ch3 is
 
    procedure Array_Type_Declaration (T : in out Entity_Id; Def : Node_Id) is
       Component_Def : constant Node_Id := Component_Definition (Def);
+      Component_Typ : constant Node_Id := Subtype_Indication (Component_Def);
       Element_Type  : Entity_Id;
       Implicit_Base : Entity_Id;
       Index         : Node_Id;
@@ -4420,7 +4731,7 @@ package body Sem_Ch3 is
       --  as prefix.
 
       if No (T) then
-         Related_Id :=  Defining_Identifier (P);
+         Related_Id := Defining_Identifier (P);
       else
          Related_Id := T;
       end if;
@@ -4429,6 +4740,10 @@ package body Sem_Ch3 is
       while Present (Index) loop
          Analyze (Index);
 
+         if not Nkind_In (Index, N_Identifier, N_Expanded_Name) then
+            Check_SPARK_Restriction ("subtype mark required", Index);
+         end if;
+
          --  Add a subtype declaration for each index of private array type
          --  declaration whose etype is also private. For example:
 
@@ -4497,10 +4812,14 @@ package body Sem_Ch3 is
 
       --  Process subtype indication if one is present
 
-      if Present (Subtype_Indication (Component_Def)) then
-         Element_Type :=
-           Process_Subtype
-             (Subtype_Indication (Component_Def), P, Related_Id, 'C');
+      if Present (Component_Typ) then
+         Element_Type := Process_Subtype (Component_Typ, P, Related_Id, 'C');
+
+         Set_Etype (Component_Typ, Element_Type);
+
+         if not Nkind_In (Component_Typ, N_Identifier, N_Expanded_Name) then
+            Check_SPARK_Restriction ("subtype mark required", Component_Typ);
+         end if;
 
       --  Ada 2005 (AI-230): Access Definition case
 
@@ -4608,6 +4927,8 @@ package body Sem_Ch3 is
       Set_Packed_Array_Type (T, Empty);
 
       if Aliased_Present (Component_Definition (Def)) then
+         Check_SPARK_Restriction
+           ("aliased is not allowed", Component_Definition (Def));
          Set_Has_Aliased_Components (Etype (T));
       end if;
 
@@ -6718,35 +7039,32 @@ package body Sem_Ch3 is
       Derived_Type : Entity_Id;
       Derive_Subps : Boolean := True)
    is
-      Loc          : constant Source_Ptr := Sloc (N);
-      Parent_Base  : Entity_Id;
-      Type_Def     : Node_Id;
-      Indic        : Node_Id;
-      Discrim      : Entity_Id;
-      Last_Discrim : Entity_Id;
-      Constrs      : Elist_Id;
-
-      Discs : Elist_Id := New_Elmt_List;
-      --  An empty Discs list means that there were no constraints in the
-      --  subtype indication or that there was an error processing it.
-
-      Assoc_List : Elist_Id;
-      New_Discrs : Elist_Id;
-      New_Base   : Entity_Id;
-      New_Decl   : Node_Id;
-      New_Indic  : Node_Id;
-
-      Is_Tagged          : constant Boolean := Is_Tagged_Type (Parent_Type);
       Discriminant_Specs : constant Boolean :=
                              Present (Discriminant_Specifications (N));
+      Is_Tagged          : constant Boolean := Is_Tagged_Type (Parent_Type);
+      Loc                : constant Source_Ptr := Sloc (N);
       Private_Extension  : constant Boolean :=
                              Nkind (N) = N_Private_Extension_Declaration;
-
+      Assoc_List         : Elist_Id;
       Constraint_Present : Boolean;
+      Constrs            : Elist_Id;
+      Discrim            : Entity_Id;
+      Indic              : Node_Id;
       Inherit_Discrims   : Boolean := False;
+      Last_Discrim       : Entity_Id;
+      New_Base           : Entity_Id;
+      New_Decl           : Node_Id;
+      New_Discrs         : Elist_Id;
+      New_Indic          : Node_Id;
+      Parent_Base        : Entity_Id;
       Save_Etype         : Entity_Id;
       Save_Discr_Constr  : Elist_Id;
       Save_Next_Entity   : Entity_Id;
+      Type_Def           : Node_Id;
+
+      Discs : Elist_Id := New_Elmt_List;
+      --  An empty Discs list means that there were no constraints in the
+      --  subtype indication or that there was an error processing it.
 
    begin
       if Ekind (Parent_Type) = E_Record_Type_With_Private
@@ -6758,6 +7076,28 @@ package body Sem_Ch3 is
          Parent_Base := Base_Type (Parent_Type);
       end if;
 
+      --  AI05-0115 : if this is a derivation from a private type in some
+      --  other scope that may lead to invisible components for the derived
+      --  type, mark it accordingly.
+
+      if Is_Private_Type (Parent_Type) then
+         if Scope (Parent_Type) = Scope (Derived_Type) then
+            null;
+
+         elsif In_Open_Scopes (Scope (Parent_Type))
+           and then In_Private_Part (Scope (Parent_Type))
+         then
+            null;
+
+         else
+            Set_Has_Private_Ancestor (Derived_Type);
+         end if;
+
+      else
+         Set_Has_Private_Ancestor
+           (Derived_Type, Has_Private_Ancestor (Parent_Type));
+      end if;
+
       --  Before we start the previously documented transformations, here is
       --  little fix for size and alignment of tagged types. Normally when we
       --  derive type D from type P, we copy the size and alignment of P as the
@@ -6986,14 +7326,18 @@ package body Sem_Ch3 is
          Analyze (N);
 
          --  Derivation of subprograms must be delayed until the full subtype
-         --  has been established to ensure proper overriding of subprograms
+         --  has been established, to ensure proper overriding of subprograms
          --  inherited by full types. If the derivations occurred as part of
          --  the call to Build_Derived_Type above, then the check for type
          --  conformance would fail because earlier primitive subprograms
          --  could still refer to the full type prior the change to the new
          --  subtype and hence would not match the new base type created here.
+         --  Subprograms are not derived, however, when Derive_Subps is False
+         --  (since otherwise there could be redundant derivations).
 
-         Derive_Subprograms (Parent_Type, Derived_Type);
+         if Derive_Subps then
+            Derive_Subprograms (Parent_Type, Derived_Type);
+         end if;
 
          --  For tagged types the Discriminant_Constraint of the new base itype
          --  is inherited from the first subtype so that no subtype conformance
@@ -7594,6 +7938,8 @@ package body Sem_Ch3 is
             Set_Stored_Constraint
               (Derived_Type, Expand_To_Stored_Constraint (Parent_Type, Discs));
             Replace_Components (Derived_Type, New_Decl);
+            Set_Has_Implicit_Dereference
+              (Derived_Type, Has_Implicit_Dereference (Parent_Type));
          end if;
 
          --  Insert the new derived type declaration
@@ -7685,28 +8031,6 @@ package body Sem_Ch3 is
          Set_Last_Entity
            (Class_Wide_Type (Derived_Type), Last_Entity (Derived_Type));
       end if;
-
-      --  Update the scope of anonymous access types of discriminants and other
-      --  components, to prevent scope anomalies in gigi, when the derivation
-      --  appears in a scope nested within that of the parent.
-
-      declare
-         D : Entity_Id;
-
-      begin
-         D := First_Entity (Derived_Type);
-         while Present (D) loop
-            if Ekind_In (D, E_Discriminant, E_Component) then
-               if Is_Itype (Etype (D))
-                  and then Ekind (Etype (D)) = E_Anonymous_Access_Type
-               then
-                  Set_Scope (Etype (D), Current_Scope);
-               end if;
-            end if;
-
-            Next_Entity (D);
-         end loop;
-      end;
    end Build_Derived_Record_Type;
 
    ------------------------
@@ -7725,18 +8049,23 @@ package body Sem_Ch3 is
    begin
       --  Set common attributes
 
-      Set_Scope         (Derived_Type, Current_Scope);
+      Set_Scope          (Derived_Type, Current_Scope);
 
-      Set_Ekind         (Derived_Type, Ekind    (Parent_Base));
-      Set_Etype         (Derived_Type,           Parent_Base);
-      Set_Has_Task      (Derived_Type, Has_Task (Parent_Base));
+      Set_Ekind          (Derived_Type, Ekind    (Parent_Base));
+      Set_Etype          (Derived_Type,           Parent_Base);
+      Set_Has_Task       (Derived_Type, Has_Task (Parent_Base));
 
       Set_Size_Info      (Derived_Type,                 Parent_Type);
       Set_RM_Size        (Derived_Type, RM_Size        (Parent_Type));
-      Set_Convention     (Derived_Type, Convention     (Parent_Type));
       Set_Is_Controlled  (Derived_Type, Is_Controlled  (Parent_Type));
       Set_Is_Tagged_Type (Derived_Type, Is_Tagged_Type (Parent_Type));
 
+      --  If the parent type is a private subtype, the convention on the base
+      --  type may be set in the private part, and not propagated to the
+      --  subtype until later, so we obtain the convention from the base type.
+
+      Set_Convention     (Derived_Type, Convention     (Parent_Base));
+
       --  Propagate invariant information. The new type has invariants if
       --  they are inherited from the parent type, and these invariants can
       --  be further inherited, so both flags are set.
@@ -8053,7 +8382,9 @@ package body Sem_Ch3 is
                --  the point of instantiation, we want to find the discriminant
                --  that corresponds to D in Rec, i.e. X.
 
-               if Present (Original_Discriminant (Id)) then
+               if Present (Original_Discriminant (Id))
+                 and then In_Instance
+               then
                   Discr := Find_Corresponding_Discriminant (Id, T);
                   Found := True;
 
@@ -8072,14 +8403,11 @@ package body Sem_Ch3 is
                      Error_Msg_N ("& does not match any discriminant", Id);
                      return New_Elmt_List;
 
-                  --  The following is only useful for the benefit of generic
-                  --  instances but it does not interfere with other
-                  --  processing for the non-generic case so we do it in all
-                  --  cases (for generics this statement is executed when
-                  --  processing the generic definition, see comment at the
-                  --  beginning of this if statement).
+                  --  If the parent type is a generic formal, preserve the
+                  --  name of the discriminant for subsequent instances.
+                  --  see comment at the beginning of this if statement.
 
-                  else
+                  elsif Is_Generic_Type (Root_Type (T)) then
                      Set_Original_Discriminant (Id, Discr);
                   end if;
                end if;
@@ -8301,6 +8629,8 @@ package body Sem_Ch3 is
 
       Set_First_Entity      (Def_Id, First_Entity   (T));
       Set_Last_Entity       (Def_Id, Last_Entity    (T));
+      Set_Has_Implicit_Dereference
+                            (Def_Id, Has_Implicit_Dereference (T));
 
       --  If the subtype is the completion of a private declaration, there may
       --  have been representation clauses for the partial view, and they must
@@ -8313,7 +8643,7 @@ package body Sem_Ch3 is
       end if;
 
       if Is_Tagged_Type (T) then
-         Set_Is_Tagged_Type  (Def_Id);
+         Set_Is_Tagged_Type (Def_Id);
          Make_Class_Wide_Type (Def_Id);
       end if;
 
@@ -8384,8 +8714,15 @@ package body Sem_Ch3 is
    is
       IR : constant Node_Id := Make_Itype_Reference (Sloc (Nod));
    begin
-      Set_Itype (IR, Ityp);
-      Insert_After (Nod, IR);
+
+      --  Itype references are only created for use by the back-end
+
+      if Inside_A_Generic then
+         return;
+      else
+         Set_Itype (IR, Ityp);
+         Insert_After (Nod, IR);
+      end if;
    end Build_Itype_Reference;
 
    ------------------------
@@ -8570,17 +8907,27 @@ package body Sem_Ch3 is
       procedure Check_Pragma_Implemented (Subp : Entity_Id) is
          Iface_Alias : constant Entity_Id := Interface_Alias (Subp);
          Impl_Kind   : constant Name_Id   := Implementation_Kind (Iface_Alias);
+         Subp_Alias  : constant Entity_Id := Alias (Subp);
          Contr_Typ   : Entity_Id;
+         Impl_Subp   : Entity_Id;
 
       begin
          --  Subp must have an alias since it is a hidden entity used to link
          --  an interface subprogram to its overriding counterpart.
 
-         pragma Assert (Present (Alias (Subp)));
+         pragma Assert (Present (Subp_Alias));
+
+         --  Handle aliases to synchronized wrappers
+
+         Impl_Subp := Subp_Alias;
+
+         if Is_Primitive_Wrapper (Impl_Subp) then
+            Impl_Subp := Wrapped_Entity (Impl_Subp);
+         end if;
 
          --  Extract the type of the controlling formal
 
-         Contr_Typ := Etype (First_Formal (Alias (Subp)));
+         Contr_Typ := Etype (First_Formal (Subp_Alias));
 
          if Is_Concurrent_Record_Type (Contr_Typ) then
             Contr_Typ := Corresponding_Concurrent_Type (Contr_Typ);
@@ -8590,12 +8937,12 @@ package body Sem_Ch3 is
          --  be implemented by an entry.
 
          if Impl_Kind = Name_By_Entry
-           and then Ekind (Wrapped_Entity (Alias (Subp))) /= E_Entry
+           and then Ekind (Impl_Subp) /= E_Entry
          then
             Error_Msg_Node_2 := Iface_Alias;
             Error_Msg_NE
               ("type & must implement abstract subprogram & with an entry",
-               Alias (Subp), Contr_Typ);
+               Subp_Alias, Contr_Typ);
 
          elsif Impl_Kind = Name_By_Protected_Procedure then
 
@@ -8607,19 +8954,17 @@ package body Sem_Ch3 is
                Error_Msg_Node_2 := Contr_Typ;
                Error_Msg_NE
                  ("interface subprogram & cannot be implemented by a " &
-                  "primitive procedure of task type &", Alias (Subp),
+                  "primitive procedure of task type &", Subp_Alias,
                   Iface_Alias);
 
             --  An interface subprogram whose implementation kind is By_
             --  Protected_Procedure must be implemented by a procedure.
 
-            elsif Is_Primitive_Wrapper (Alias (Subp))
-              and then Ekind (Wrapped_Entity (Alias (Subp))) /= E_Procedure
-            then
+            elsif Ekind (Impl_Subp) /= E_Procedure then
                Error_Msg_Node_2 := Iface_Alias;
                Error_Msg_NE
                  ("type & must implement abstract subprogram & with a " &
-                  "procedure", Alias (Subp), Contr_Typ);
+                  "procedure", Subp_Alias, Contr_Typ);
             end if;
          end if;
       end Check_Pragma_Implemented;
@@ -8639,10 +8984,11 @@ package body Sem_Ch3 is
          --  Ada 2012 (AI05-0030): The implementation kinds of an overridden
          --  and overriding subprogram are different. In general this is an
          --  error except when the implementation kind of the overridden
-         --  subprograms is By_Any.
+         --  subprograms is By_Any or Optional.
 
          if Iface_Kind /= Subp_Kind
            and then Iface_Kind /= Name_By_Any
+           and then Iface_Kind /= Name_Optional
          then
             if Iface_Kind = Name_By_Entry then
                Error_Msg_N
@@ -8720,7 +9066,7 @@ package body Sem_Ch3 is
          --  The partial view of T may have been a private extension, for
          --  which inherited functions dispatching on result are abstract.
          --  If the full view is a null extension, there is no need for
-         --  overriding in Ada2005, but wrappers need to be built for them
+         --  overriding in Ada 2005, but wrappers need to be built for them
          --  (see exp_ch3, Build_Controlling_Function_Wrappers).
 
          if Is_Null_Extension (T)
@@ -8819,16 +9165,36 @@ package body Sem_Ch3 is
                         begin
                            E := Subp;
                            while Present (Alias (E)) loop
-                              Error_Msg_Sloc := Sloc (E);
-                              Error_Msg_NE
-                                ("\& has been inherited #", T, Subp);
+
+                              --  Avoid reporting redundant errors on entities
+                              --  inherited from interfaces
+
+                              if Sloc (E) /= Sloc (T) then
+                                 Error_Msg_Sloc := Sloc (E);
+                                 Error_Msg_NE
+                                   ("\& has been inherited #", T, Subp);
+                              end if;
+
                               E := Alias (E);
                            end loop;
 
                            Error_Msg_Sloc := Sloc (E);
-                           Error_Msg_NE
-                             ("\& has been inherited from subprogram #",
-                              T, Subp);
+
+                           --  AI05-0068: report if there is an overriding
+                           --  non-abstract subprogram that is invisible.
+
+                           if Is_Hidden (E)
+                             and then not Is_Abstract_Subprogram (E)
+                           then
+                              Error_Msg_NE
+                                ("\& subprogram# is not visible",
+                                 T, Subp);
+
+                           else
+                              Error_Msg_NE
+                                ("\& has been inherited from subprogram #",
+                                 T, Subp);
+                           end if;
                         end;
                      end if;
                   end if;
@@ -8842,19 +9208,14 @@ package body Sem_Ch3 is
                   --  The controlling formal of Subp must be of mode "out",
                   --  "in out" or an access-to-variable to be overridden.
 
-                  --  Error message below needs rewording (remember comma
-                  --  in -gnatj mode) ???
-
                   if Ekind (First_Formal (Subp)) = E_In_Parameter
                     and then Ekind (Subp) /= E_Function
                   then
-                     if not Is_Predefined_Dispatching_Operation (Subp) then
-                        Error_Msg_NE
-                          ("first formal of & must be of mode `OUT`, " &
-                           "`IN OUT` or access-to-variable", T, Subp);
-                        Error_Msg_N
-                          ("\to be overridden by protected procedure or " &
-                           "entry (RM 9.4(11.9/2))", T);
+                     if not Is_Predefined_Dispatching_Operation (Subp)
+                       and then Is_Protected_Type
+                                  (Corresponding_Concurrent_Type (T))
+                     then
+                        Error_Msg_PT (T, Subp);
                      end if;
 
                   --  Some other kind of overriding failure
@@ -9191,6 +9552,7 @@ package body Sem_Ch3 is
          --  In case of previous errors, other expansion actions that provide
          --  bodies for null procedures with not be invoked, so inhibit message
          --  in those cases.
+
          --  Note that E_Operator is not in the list that follows, because
          --  this kind is reserved for predefined operators, that are
          --  intrinsic and do not need completion.
@@ -9248,8 +9610,12 @@ package body Sem_Ch3 is
                May_Need_Implicit_Body (E);
             end if;
 
+         --  A formal incomplete type (Ada 2012) does not require a completion;
+         --  other incomplete type declarations do.
+
          elsif Ekind (E) = E_Incomplete_Type
            and then No (Underlying_Type (E))
+           and then not Is_Generic_Type (E)
          then
             Post_Error;
 
@@ -9293,6 +9659,40 @@ package body Sem_Ch3 is
       end loop;
    end Check_Completion;
 
+   ------------------------------------
+   -- Check_CPP_Type_Has_No_Defaults --
+   ------------------------------------
+
+   procedure Check_CPP_Type_Has_No_Defaults (T : Entity_Id) is
+      Tdef  : constant Node_Id := Type_Definition (Declaration_Node (T));
+      Clist : Node_Id;
+      Comp  : Node_Id;
+
+   begin
+      --  Obtain the component list
+
+      if Nkind (Tdef) = N_Record_Definition then
+         Clist := Component_List (Tdef);
+      else pragma Assert (Nkind (Tdef) = N_Derived_Type_Definition);
+         Clist := Component_List (Record_Extension_Part (Tdef));
+      end if;
+
+      --  Check all components to ensure no default expressions
+
+      if Present (Clist) then
+         Comp := First (Component_Items (Clist));
+         while Present (Comp) loop
+            if Present (Expression (Comp)) then
+               Error_Msg_N
+                 ("component of imported 'C'P'P type cannot have "
+                  & "default expression", Expression (Comp));
+            end if;
+
+            Next (Comp);
+         end loop;
+      end if;
+   end Check_CPP_Type_Has_No_Defaults;
+
    ----------------------------
    -- Check_Delta_Expression --
    ----------------------------
@@ -9369,9 +9769,25 @@ package body Sem_Ch3 is
                  ("?cannot initialize entities of limited type!", Exp);
 
             elsif Ada_Version < Ada_2005 then
-               Error_Msg_N
-                 ("cannot initialize entities of limited type", Exp);
-               Explain_Limited_Type (T, Exp);
+
+               --  The side effect removal machinery may generate illegal Ada
+               --  code to avoid the usage of access types and 'reference in
+               --  Alfa mode. Since this is legal code with respect to theorem
+               --  proving, do not emit the error.
+
+               if Alfa_Mode
+                 and then Nkind (Exp) = N_Function_Call
+                 and then Nkind (Parent (Exp)) = N_Object_Declaration
+                 and then not Comes_From_Source
+                                (Defining_Identifier (Parent (Exp)))
+               then
+                  null;
+
+               else
+                  Error_Msg_N
+                    ("cannot initialize entities of limited type", Exp);
+                  Explain_Limited_Type (T, Exp);
+               end if;
 
             else
                --  Specialize error message according to kind of illegal
@@ -9815,9 +10231,10 @@ package body Sem_Ch3 is
       Set_Homonym     (Full, Save_Homonym);
       Set_Associated_Node_For_Itype (Full, Related_Nod);
 
-      --  Set common attributes for all subtypes
+      --  Set common attributes for all subtypes: kind, convention, etc.
 
       Set_Ekind (Full, Subtype_Kind (Ekind (Full_Base)));
+      Set_Convention (Full, Convention (Full_Base));
 
       --  The Etype of the full view is inconsistent. Gigi needs to see the
       --  structural full view,  which is what the current scheme gives:
@@ -9988,6 +10405,7 @@ package body Sem_Ch3 is
       --  type, so we must be sure not to overwrite these entries.
 
       declare
+         Append    : Boolean;
          Item      : Node_Id;
          Next_Item : Node_Id;
 
@@ -10000,18 +10418,35 @@ package body Sem_Ch3 is
          if No (Item) then
             Set_First_Rep_Item (Full, First_Rep_Item (Priv));
 
-         --  Else search to end of items currently linked to the full subtype
+         --  Otherwise, search to the end of items currently linked to the full
+         --  subtype and append the private items to the end. However, if Priv
+         --  and Full already have the same list of rep items, then the append
+         --  is not done, as that would create a circularity.
+
+         elsif Item /= First_Rep_Item (Priv) then
+            Append := True;
 
-         else
             loop
                Next_Item := Next_Rep_Item (Item);
                exit when No (Next_Item);
                Item := Next_Item;
+
+               --  If the private view has aspect specifications, the full view
+               --  inherits them. Since these aspects may already have been
+               --  attached to the full view during derivation, do not append
+               --  them if already present.
+
+               if Item = First_Rep_Item (Priv) then
+                  Append := False;
+                  exit;
+               end if;
             end loop;
 
             --  And link the private type items at the end of the chain
 
-            Set_Next_Rep_Item (Item, First_Rep_Item (Priv));
+            if Append then
+               Set_Next_Rep_Item (Item, First_Rep_Item (Priv));
+            end if;
          end if;
       end;
 
@@ -10320,24 +10755,24 @@ package body Sem_Ch3 is
             return;
          end if;
 
+         --  Enforce rule that the constraint is illegal if there is an
+         --  unconstrained view of the designated type. This means that the
+         --  partial view (either a private type declaration or a derivation
+         --  from a private type) has no discriminants. (Defect Report
+         --  8652/0008, Technical Corrigendum 1, checked by ACATS B371001).
+
+         --  Rule updated for Ada 2005: the private type is said to have
+         --  a constrained partial view, given that objects of the type
+         --  can be declared. Furthermore, the rule applies to all access
+         --  types, unlike the rule concerning default discriminants (see
+         --  RM 3.7.1(7/3))
+
          if (Ekind (T) = E_General_Access_Type
               or else Ada_Version >= Ada_2005)
            and then Has_Private_Declaration (Desig_Type)
            and then In_Open_Scopes (Scope (Desig_Type))
            and then Has_Discriminants (Desig_Type)
          then
-            --  Enforce rule that the constraint is illegal if there is
-            --  an unconstrained view of the designated type. This means
-            --  that the partial view (either a private type declaration or
-            --  a derivation from a private type) has no discriminants.
-            --  (Defect Report 8652/0008, Technical Corrigendum 1, checked
-            --  by ACATS B371001).
-
-            --  Rule updated for Ada 2005: the private type is said to have
-            --  a constrained partial view, given that objects of the type
-            --  can be declared. Furthermore, the rule applies to all access
-            --  types, unlike the rule concerning default discriminants.
-
             declare
                Pack  : constant Node_Id :=
                          Unit_Declaration_Node (Scope (Desig_Type));
@@ -10365,9 +10800,8 @@ package body Sem_Ch3 is
                      then
                         if No (Discriminant_Specifications (Decl)) then
                            Error_Msg_N
-                            ("cannot constrain general access type if " &
-                               "designated type has constrained partial view",
-                                S);
+                            ("cannot constrain access type if designated " &
+                               "type has constrained partial view", S);
                         end if;
 
                         exit;
@@ -11006,7 +11440,10 @@ package body Sem_Ch3 is
       Related_Id  : Entity_Id;
       Suffix      : Character)
    is
-      T_Ent : Entity_Id := Entity (Subtype_Mark (SI));
+      --  Retrieve Base_Type to ensure getting to the concurrent type in the
+      --  case of a private subtype (needed when only doing semantic analysis).
+
+      T_Ent : Entity_Id := Base_Type (Entity (Subtype_Mark (SI)));
       T_Val : Entity_Id;
 
    begin
@@ -11107,6 +11544,9 @@ package body Sem_Ch3 is
 
       else
          pragma Assert (Nkind (C) = N_Digits_Constraint);
+
+         Check_SPARK_Restriction ("digits constraint is not allowed", S);
+
          Digits_Expr := Digits_Expression (C);
          Analyze_And_Resolve (Digits_Expr, Any_Integer);
 
@@ -11333,6 +11773,8 @@ package body Sem_Ch3 is
       --  Digits constraint present
 
       if Nkind (C) = N_Digits_Constraint then
+
+         Check_SPARK_Restriction ("digits constraint is not allowed", S);
          Check_Restriction (No_Obsolescent_Features, C);
 
          if Warn_On_Obsolescent_Feature then
@@ -11404,7 +11846,7 @@ package body Sem_Ch3 is
           (Nkind (S) = N_Attribute_Reference
             and then Attribute_Name (S) = Name_Range)
       then
-         --  A Range attribute will transformed into N_Range by Resolve
+         --  A Range attribute will be transformed into N_Range by Resolve
 
          Analyze (S);
          Set_Etype (S, T);
@@ -11433,6 +11875,20 @@ package body Sem_Ch3 is
          Resolve_Discrete_Subtype_Indication (S, T);
          R := Range_Expression (Constraint (S));
 
+         --  Capture values of bounds and generate temporaries for them if
+         --  needed, since checks may cause duplication of the expressions
+         --  which must not be reevaluated.
+
+         --  The forced evaluation removes side effects from expressions,
+         --  which should occur also in Alfa mode. Otherwise, we end up with
+         --  unexpected insertions of actions at places where this is not
+         --  supposed to occur, e.g. on default parameters of a call.
+
+         if Expander_Active then
+            Force_Evaluation (Low_Bound (R));
+            Force_Evaluation (High_Bound (R));
+         end if;
+
       elsif Nkind (S) = N_Discriminant_Association then
 
          --  Syntactically valid in subtype indication
@@ -11544,6 +12000,8 @@ package body Sem_Ch3 is
       --  Delta constraint present
 
       if Nkind (C) = N_Delta_Constraint then
+
+         Check_SPARK_Restriction ("delta constraint is not allowed", S);
          Check_Restriction (No_Obsolescent_Features, C);
 
          if Warn_On_Obsolescent_Feature then
@@ -11874,8 +12332,8 @@ package body Sem_Ch3 is
             Next_Discriminant (Old_C);
          end loop;
 
-         --  The tag, and the possible parent and controller components
-         --  are unconditionally in the subtype.
+         --  The tag and the possible parent component are unconditionally in
+         --  the subtype.
 
          if Is_Tagged_Type (Typ)
            or else Has_Controlled_Component (Typ)
@@ -11884,7 +12342,6 @@ package body Sem_Ch3 is
             while Present (Old_C) loop
                if Chars ((Old_C)) = Name_uTag
                  or else Chars ((Old_C)) = Name_uParent
-                 or else Chars ((Old_C)) = Name_uController
                then
                   Append_Elmt (Old_C, Comp_List);
                end if;
@@ -12150,7 +12607,6 @@ package body Sem_Ch3 is
                if Original_Record_Component (Old_C) = Old_C
                 and then Chars (Old_C) /= Name_uTag
                 and then Chars (Old_C) /= Name_uParent
-                and then Chars (Old_C) /= Name_uController
                then
                   Append_Elmt (Old_C, Comp_List);
                end if;
@@ -12200,6 +12656,8 @@ package body Sem_Ch3 is
       Bound_Val     : Ureal;
 
    begin
+      Check_SPARK_Restriction
+        ("decimal fixed point type is not allowed", Def);
       Check_Restriction (No_Fixed_Point, Def);
 
       --  Create implicit base type
@@ -12423,14 +12881,15 @@ package body Sem_Ch3 is
                Iface_Subp := Node (Prim_Elmt);
 
                --  Exclude derivation of predefined primitives except those
-               --  that come from source. Required to catch declarations of
-               --  equality operators of interfaces. For example:
+               --  that come from source, or are inherited from one that comes
+               --  from source. Required to catch declarations of equality
+               --  operators of interfaces. For example:
 
                --     type Iface is interface;
                --     function "=" (Left, Right : Iface) return Boolean;
 
                if not Is_Predefined_Dispatching_Operation (Iface_Subp)
-                 or else Comes_From_Source (Iface_Subp)
+                 or else Comes_From_Source (Ultimate_Alias (Iface_Subp))
                then
                   E := Find_Primitive_Covering_Interface
                          (Tagged_Type => Tagged_Type,
@@ -12696,6 +13155,7 @@ package body Sem_Ch3 is
       New_Subp :=
          New_Entity (Nkind (Parent_Subp), Sloc (Derived_Type));
       Set_Ekind (New_Subp, Ekind (Parent_Subp));
+      Set_Contract (New_Subp, Make_Contract (Sloc (New_Subp)));
 
       --  Check whether the inherited subprogram is a private operation that
       --  should be inherited but not yet made visible. Such subprograms can
@@ -12979,18 +13439,18 @@ package body Sem_Ch3 is
 
       --  Check for case of a derived subprogram for the instantiation of a
       --  formal derived tagged type, if so mark the subprogram as dispatching
-      --  and inherit the dispatching attributes of the parent subprogram. The
+      --  and inherit the dispatching attributes of the actual subprogram. The
       --  derived subprogram is effectively renaming of the actual subprogram,
       --  so it needs to have the same attributes as the actual.
 
       if Present (Actual_Subp)
-        and then Is_Dispatching_Operation (Parent_Subp)
+        and then Is_Dispatching_Operation (Actual_Subp)
       then
          Set_Is_Dispatching_Operation (New_Subp);
 
-         if Present (DTC_Entity (Parent_Subp)) then
-            Set_DTC_Entity (New_Subp, DTC_Entity (Parent_Subp));
-            Set_DT_Position (New_Subp, DT_Position (Parent_Subp));
+         if Present (DTC_Entity (Actual_Subp)) then
+            Set_DTC_Entity (New_Subp, DTC_Entity (Actual_Subp));
+            Set_DT_Position (New_Subp, DT_Position (Actual_Subp));
          end if;
       end if;
 
@@ -13322,7 +13782,8 @@ package body Sem_Ch3 is
                      Type_Conformant (Subp, Act_Subp,
                                       Skip_Controlling_Formals => True)))
             then
-               pragma Assert (not Is_Ancestor (Parent_Base, Generic_Actual));
+               pragma Assert (not Is_Ancestor (Parent_Base, Generic_Actual,
+                                               Use_Full_View => True));
 
                --  Remember that we need searching for all pending primitives
 
@@ -13693,7 +14154,6 @@ package body Sem_Ch3 is
       Indic        : constant Node_Id := Subtype_Indication (Def);
       Extension    : constant Node_Id := Record_Extension_Part (Def);
       Parent_Node  : Node_Id;
-      Parent_Scope : Entity_Id;
       Taggd        : Boolean;
 
    --  Start of processing for Derived_Type_Declaration
@@ -13705,6 +14165,8 @@ package body Sem_Ch3 is
       --  parent is also an interface.
 
       if Interface_Present (Def) then
+         Check_SPARK_Restriction ("interface is not allowed", Def);
+
          if not Is_Interface (Parent_Type) then
             Diagnose_Interface (Indic, Parent_Type);
 
@@ -13945,17 +14407,20 @@ package body Sem_Ch3 is
       end if;
 
       --  Only composite types other than array types are allowed to have
-      --  discriminants.
+      --  discriminants. In SPARK, no types are allowed to have discriminants.
 
-      if Present (Discriminant_Specifications (N))
-        and then (Is_Elementary_Type (Parent_Type)
-                  or else Is_Array_Type (Parent_Type))
-        and then not Error_Posted (N)
-      then
-         Error_Msg_N
-           ("elementary or array type cannot have discriminants",
-            Defining_Identifier (First (Discriminant_Specifications (N))));
-         Set_Has_Discriminants (T, False);
+      if Present (Discriminant_Specifications (N)) then
+         if (Is_Elementary_Type (Parent_Type)
+              or else Is_Array_Type (Parent_Type))
+           and then not Error_Posted (N)
+         then
+            Error_Msg_N
+              ("elementary or array type cannot have discriminants",
+               Defining_Identifier (First (Discriminant_Specifications (N))));
+            Set_Has_Discriminants (T, False);
+         else
+            Check_SPARK_Restriction ("discriminant type is not allowed", N);
+         end if;
       end if;
 
       --  In Ada 83, a derived type defined in a package specification cannot
@@ -13983,10 +14448,10 @@ package body Sem_Ch3 is
         or else Has_Private_Component (Parent_Type)
       then
          --  The ancestor type of a formal type can be incomplete, in which
-         --  case only the operations of the partial view are available in
-         --  the generic. Subsequent checks may be required when the full
-         --  view is analyzed, to verify that derivation from a tagged type
-         --  has an extension.
+         --  case only the operations of the partial view are available in the
+         --  generic. Subsequent checks may be required when the full view is
+         --  analyzed to verify that a derivation from a tagged type has an
+         --  extension.
 
          if Nkind (Original_Node (N)) = N_Formal_Type_Declaration then
             null;
@@ -14010,25 +14475,18 @@ package body Sem_Ch3 is
          --  that it is not a Full_Type_Declaration (i.e. a private type or
          --  private extension declaration), to distinguish a partial view
          --  from  a derivation from a private type which also appears as
-         --  E_Private_Type.
+         --  E_Private_Type. If the parent base type is not declared in an
+         --  enclosing scope there is no need to check.
 
          elsif Present (Full_View (Parent_Type))
            and then Nkind (Parent (Parent_Type)) /= N_Full_Type_Declaration
            and then not Is_Tagged_Type (Parent_Type)
            and then Is_Tagged_Type (Full_View (Parent_Type))
+           and then In_Open_Scopes (Scope (Base_Type (Parent_Type)))
          then
-            Parent_Scope := Scope (T);
-            while Present (Parent_Scope)
-              and then Parent_Scope /= Standard_Standard
-            loop
-               if Parent_Scope = Scope (Parent_Type) then
-                  Error_Msg_N
-                    ("premature derivation from type with tagged full view",
-                     Indic);
-               end if;
-
-               Parent_Scope := Scope (Parent_Scope);
-            end loop;
+            Error_Msg_N
+              ("premature derivation from type with tagged full view",
+                Indic);
          end if;
       end if;
 
@@ -14147,6 +14605,13 @@ package body Sem_Ch3 is
             end if;
          end if;
       end if;
+
+      --  In SPARK, there are no derived type definitions other than type
+      --  extensions of tagged record types.
+
+      if No (Extension) then
+         Check_SPARK_Restriction ("derived type is not allowed", N);
+      end if;
    end Derived_Type_Declaration;
 
    ------------------------
@@ -14487,7 +14952,7 @@ package body Sem_Ch3 is
                Error_Msg_NE ("invalid redeclaration of }", Id, Prev);
             end if;
 
-            Set_Full_View (Prev,  Id);
+            Set_Full_View (Prev, Id);
             Append_Entity (Id, Current_Scope);
             Set_Is_Public (Id, Is_Public (Prev));
             Set_Is_Internal (Id);
@@ -14503,7 +14968,15 @@ package body Sem_Ch3 is
             then
                Set_Ekind (Id, Ekind (Prev));         --  will be reset later
                Set_Class_Wide_Type (Id, Class_Wide_Type (Prev));
-               Set_Etype (Class_Wide_Type (Id), Id);
+
+               --  If the incomplete type is completed by a private declaration
+               --  the class-wide type remains associated with the incomplete
+               --  type, to prevent order-of-elaboration issues in gigi, else
+               --  we associate the class-wide type with the known full view.
+
+               if Nkind (N) /= N_Private_Type_Declaration then
+                  Set_Etype (Class_Wide_Type (Id), Id);
+               end if;
             end if;
 
          --  Case of full declaration of private type
@@ -14591,6 +15064,12 @@ package body Sem_Ch3 is
             Set_Has_Private_Declaration (Prev);
             Set_Has_Private_Declaration (Id);
 
+            --  Preserve aspect and iterator flags that may have been set on
+            --  the partial view.
+
+            Set_Has_Delayed_Aspects (Prev, Has_Delayed_Aspects (Id));
+            Set_Has_Implicit_Dereference (Prev, Has_Implicit_Dereference (Id));
+
             --  If no error, propagate freeze_node from private to full view.
             --  It may have been generated for an early operational item.
 
@@ -14695,6 +15174,15 @@ package body Sem_Ch3 is
             end if;
          end if;
 
+         if Present (Prev)
+           and then Nkind (Parent (Prev)) = N_Incomplete_Type_Declaration
+           and then Present (Premature_Use (Parent (Prev)))
+         then
+            Error_Msg_Sloc := Sloc (N);
+            Error_Msg_N
+              ("\full declaration #", Premature_Use (Parent (Prev)));
+         end if;
+
          return New_Id;
       end if;
    end Find_Type_Name;
@@ -14775,12 +15263,30 @@ package body Sem_Ch3 is
 
       elsif Def_Kind = N_Access_Definition then
          T := Access_Definition (Related_Nod, Obj_Def);
-         Set_Is_Local_Anonymous_Access (T);
+
+         Set_Is_Local_Anonymous_Access
+           (T,
+            V => (Ada_Version < Ada_2012)
+                   or else (Nkind (P) /= N_Object_Declaration)
+                   or else Is_Library_Level_Entity (Defining_Identifier (P)));
 
       --  Otherwise, the object definition is just a subtype_mark
 
       else
          T := Process_Subtype (Obj_Def, Related_Nod);
+
+         --  If expansion is disabled an object definition that is an aggregate
+         --  will not get expanded and may lead to scoping problems in the back
+         --  end, if the object is referenced in an inner scope. In that case
+         --  create an itype reference for the object definition now. This
+         --  may be redundant in some cases, but harmless.
+
+         if Is_Itype (T)
+           and then Nkind (Related_Nod) = N_Object_Declaration
+           and then ASIS_Mode
+         then
+            Build_Itype_Reference (T, Related_Nod);
+         end if;
       end if;
 
       return T;
@@ -14832,13 +15338,19 @@ package body Sem_Ch3 is
 
    procedure Floating_Point_Type_Declaration (T : Entity_Id; Def : Node_Id) is
       Digs          : constant Node_Id := Digits_Expression (Def);
+      Max_Digs_Val  : constant Uint := Digits_Value (Standard_Long_Long_Float);
       Digs_Val      : Uint;
       Base_Typ      : Entity_Id;
       Implicit_Base : Entity_Id;
       Bound         : Node_Id;
 
       function Can_Derive_From (E : Entity_Id) return Boolean;
-      --  Find if given digits value allows derivation from specified type
+      --  Find if given digits value, and possibly a specified range, allows
+      --  derivation from specified type
+
+      function Find_Base_Type return Entity_Id;
+      --  Find a predefined base type that Def can derive from, or generate
+      --  an error and substitute Long_Long_Float if none exists.
 
       ---------------------
       -- Can_Derive_From --
@@ -14848,10 +15360,23 @@ package body Sem_Ch3 is
          Spec : constant Entity_Id := Real_Range_Specification (Def);
 
       begin
+         --  Check specified "digits" constraint
+
          if Digs_Val > Digits_Value (E) then
             return False;
          end if;
 
+         --  Avoid types not matching pragma Float_Representation, if present
+
+         if (Opt.Float_Format = 'I' and then Float_Rep (E) /= IEEE_Binary)
+              or else
+            (Opt.Float_Format = 'V' and then Float_Rep (E) /= VAX_Native)
+         then
+            return False;
+         end if;
+
+         --  Check for matching range, if specified
+
          if Present (Spec) then
             if Expr_Value_R (Type_Low_Bound (E)) >
                Expr_Value_R (Low_Bound (Spec))
@@ -14869,6 +15394,45 @@ package body Sem_Ch3 is
          return True;
       end Can_Derive_From;
 
+      --------------------
+      -- Find_Base_Type --
+      --------------------
+
+      function Find_Base_Type return Entity_Id is
+         Choice : Elmt_Id := First_Elmt (Predefined_Float_Types);
+
+      begin
+         --  Iterate over the predefined types in order, returning the first
+         --  one that Def can derive from.
+
+         while Present (Choice) loop
+            if Can_Derive_From (Node (Choice)) then
+               return Node (Choice);
+            end if;
+
+            Next_Elmt (Choice);
+         end loop;
+
+         --  If we can't derive from any existing type, use Long_Long_Float
+         --  and give appropriate message explaining the problem.
+
+         if Digs_Val > Max_Digs_Val then
+            --  It might be the case that there is a type with the requested
+            --  range, just not the combination of digits and range.
+
+            Error_Msg_N
+              ("no predefined type has requested range and precision",
+               Real_Range_Specification (Def));
+
+         else
+            Error_Msg_N
+              ("range too large for any predefined type",
+               Real_Range_Specification (Def));
+         end if;
+
+         return Standard_Long_Long_Float;
+      end Find_Base_Type;
+
    --  Start of processing for Floating_Point_Type_Declaration
 
    begin
@@ -14889,32 +15453,35 @@ package body Sem_Ch3 is
 
       Process_Real_Range_Specification (Def);
 
-      if Can_Derive_From (Standard_Short_Float) then
-         Base_Typ := Standard_Short_Float;
-      elsif Can_Derive_From (Standard_Float) then
-         Base_Typ := Standard_Float;
-      elsif Can_Derive_From (Standard_Long_Float) then
-         Base_Typ := Standard_Long_Float;
-      elsif Can_Derive_From (Standard_Long_Long_Float) then
-         Base_Typ := Standard_Long_Long_Float;
-
-      --  If we can't derive from any existing type, use long_long_float
-      --  and give appropriate message explaining the problem.
+      --  Check that requested number of digits is not too high.
 
-      else
-         Base_Typ := Standard_Long_Long_Float;
+      if Digs_Val > Max_Digs_Val then
+         --  The check for Max_Base_Digits may be somewhat expensive, as it
+         --  requires reading System, so only do it when necessary.
 
-         if Digs_Val >= Digits_Value (Standard_Long_Long_Float) then
-            Error_Msg_Uint_1 := Digits_Value (Standard_Long_Long_Float);
-            Error_Msg_N ("digits value out of range, maximum is ^", Digs);
+         declare
+            Max_Base_Digits : constant Uint :=
+                                Expr_Value
+                                  (Expression
+                                     (Parent (RTE (RE_Max_Base_Digits))));
 
-         else
-            Error_Msg_N
-              ("range too large for any predefined type",
-               Real_Range_Specification (Def));
-         end if;
+         begin
+            if Digs_Val > Max_Base_Digits then
+               Error_Msg_Uint_1 := Max_Base_Digits;
+               Error_Msg_N ("digits value out of range, maximum is ^", Digs);
+
+            elsif No (Real_Range_Specification (Def)) then
+               Error_Msg_Uint_1 := Max_Digs_Val;
+               Error_Msg_N ("types with more than ^ digits need range spec "
+                 & "(RM 3.5.7(6))", Digs);
+            end if;
+         end;
       end if;
 
+      --  Find a suitable type to derive from or complain and use a substitute
+
+      Base_Typ := Find_Base_Type;
+
       --  If there are bounds given in the declaration use them as the bounds
       --  of the type, otherwise use the bounds of the predefined base type
       --  that was chosen based on the Digits value.
@@ -15270,10 +15837,52 @@ package body Sem_Ch3 is
          Plain_Discrim  : Boolean := False;
          Stored_Discrim : Boolean := False)
       is
+         procedure Set_Anonymous_Type (Id : Entity_Id);
+         --  Id denotes the entity of an access discriminant or anonymous
+         --  access component. Set the type of Id to either the same type of
+         --  Old_C or create a new one depending on whether the parent and
+         --  the child types are in the same scope.
+
+         ------------------------
+         -- Set_Anonymous_Type --
+         ------------------------
+
+         procedure Set_Anonymous_Type (Id : Entity_Id) is
+            Old_Typ : constant Entity_Id := Etype (Old_C);
+
+         begin
+            if Scope (Parent_Base) = Scope (Derived_Base) then
+               Set_Etype (Id, Old_Typ);
+
+            --  The parent and the derived type are in two different scopes.
+            --  Reuse the type of the original discriminant / component by
+            --  copying it in order to preserve all attributes.
+
+            else
+               declare
+                  Typ : constant Entity_Id := New_Copy (Old_Typ);
+
+               begin
+                  Set_Etype (Id, Typ);
+
+                  --  Since we do not generate component declarations for
+                  --  inherited components, associate the itype with the
+                  --  derived type.
+
+                  Set_Associated_Node_For_Itype (Typ, Parent (Derived_Base));
+                  Set_Scope                     (Typ, Derived_Base);
+               end;
+            end if;
+         end Set_Anonymous_Type;
+
+         --  Local variables and constants
+
          New_C : constant Entity_Id := New_Copy (Old_C);
 
-         Discrim      : Entity_Id;
          Corr_Discrim : Entity_Id;
+         Discrim      : Entity_Id;
+
+      --  Start of processing for Inherit_Component
 
       begin
          pragma Assert (not Is_Tagged or else not Stored_Discrim);
@@ -15295,6 +15904,14 @@ package body Sem_Ch3 is
             Set_Original_Record_Component (New_C, New_C);
          end if;
 
+         --  Set the proper type of an access discriminant
+
+         if Ekind (New_C) = E_Discriminant
+           and then Ekind (Etype (New_C)) = E_Anonymous_Access_Type
+         then
+            Set_Anonymous_Type (New_C);
+         end if;
+
          --  If we have inherited a component then see if its Etype contains
          --  references to Parent_Base discriminants. In this case, replace
          --  these references with the constraints given in Discs. We do not
@@ -15304,10 +15921,16 @@ package body Sem_Ch3 is
          --  transformation in some error situations.
 
          if Ekind (New_C) = E_Component then
-            if (Is_Private_Type (Derived_Base)
-                 and then not Is_Generic_Type (Derived_Base))
+
+            --  Set the proper type of an anonymous access component
+
+            if Ekind (Etype (New_C)) = E_Anonymous_Access_Type then
+               Set_Anonymous_Type (New_C);
+
+            elsif (Is_Private_Type (Derived_Base)
+                    and then not Is_Generic_Type (Derived_Base))
               or else (Is_Empty_Elmt_List (Discs)
-                        and then  not Expander_Active)
+                         and then not Expander_Active)
             then
                Set_Etype (New_C, Etype (Old_C));
 
@@ -15331,7 +15954,7 @@ package body Sem_Ch3 is
                Set_Etype
                  (New_C,
                   Constrain_Component_Type
-                  (Old_C, Derived_Base, N, Parent_Base, Discs));
+                    (Old_C, Derived_Base, N, Parent_Base, Discs));
             end if;
          end if;
 
@@ -15519,6 +16142,31 @@ package body Sem_Ch3 is
    end Inherit_Components;
 
    -----------------------
+   -- Is_Constant_Bound --
+   -----------------------
+
+   function Is_Constant_Bound (Exp : Node_Id) return Boolean is
+   begin
+      if Compile_Time_Known_Value (Exp) then
+         return True;
+
+      elsif Is_Entity_Name (Exp)
+        and then Present (Entity (Exp))
+      then
+         return Is_Constant_Object (Entity (Exp))
+           or else Ekind (Entity (Exp)) = E_Enumeration_Literal;
+
+      elsif Nkind (Exp) in N_Binary_Op then
+         return Is_Constant_Bound (Left_Opnd (Exp))
+           and then Is_Constant_Bound (Right_Opnd (Exp))
+           and then Scope (Entity (Exp)) = Standard_Standard;
+
+      else
+         return False;
+      end if;
+   end Is_Constant_Bound;
+
+   -----------------------
    -- Is_Null_Extension --
    -----------------------
 
@@ -15672,13 +16320,6 @@ package body Sem_Ch3 is
       elsif not Comes_From_Source (Original_Comp) then
          return True;
 
-      --  If we are in the body of an instantiation, the component is visible
-      --  even when the parent type (possibly defined in an enclosing unit or
-      --  in a parent unit) might not.
-
-      elsif In_Instance_Body then
-         return True;
-
       --  Discriminants are always visible
 
       elsif Ekind (Original_Comp) = E_Discriminant
@@ -15686,6 +16327,12 @@ package body Sem_Ch3 is
       then
          return True;
 
+      --  In the body of an instantiation, no need to check for the visibility
+      --  of a component.
+
+      elsif In_Instance_Body then
+         return True;
+
       --  If the component has been declared in an ancestor which is currently
       --  a private type, then it is not visible. The same applies if the
       --  component's containing type is not in an open scope and the original
@@ -15769,15 +16416,31 @@ package body Sem_Ch3 is
       Next_E  : Entity_Id;
 
    begin
-      --  The class wide type can have been defined by the partial view, in
-      --  which case everything is already done.
-
       if Present (Class_Wide_Type (T)) then
-         return;
-      end if;
 
-      CW_Type :=
-        New_External_Entity (E_Void, Scope (T), Sloc (T), T, 'C', 0, 'T');
+         --  The class-wide type is a partially decorated entity created for a
+         --  unanalyzed tagged type referenced through a limited with clause.
+         --  When the tagged type is analyzed, its class-wide type needs to be
+         --  redecorated. Note that we reuse the entity created by Decorate_
+         --  Tagged_Type in order to preserve all links.
+
+         if Materialize_Entity (Class_Wide_Type (T)) then
+            CW_Type := Class_Wide_Type (T);
+            Set_Materialize_Entity (CW_Type, False);
+
+         --  The class wide type can have been defined by the partial view, in
+         --  which case everything is already done.
+
+         else
+            return;
+         end if;
+
+      --  Default case, we need to create a new class-wide type
+
+      else
+         CW_Type :=
+           New_External_Entity (E_Void, Scope (T), Sloc (T), T, 'C', 0, 'T');
+      end if;
 
       --  Inherit root type characteristics
 
@@ -15836,7 +16499,8 @@ package body Sem_Ch3 is
      (I            : Node_Id;
       Related_Nod  : Node_Id;
       Related_Id   : Entity_Id := Empty;
-      Suffix_Index : Nat := 1)
+      Suffix_Index : Nat := 1;
+      In_Iter_Schm : Boolean := False)
    is
       R      : Node_Id;
       T      : Entity_Id;
@@ -15948,7 +16612,7 @@ package body Sem_Ch3 is
          end if;
 
          R := I;
-         Process_Range_Expr_In_Decl (R, T);
+         Process_Range_Expr_In_Decl (R, T, In_Iter_Schm => In_Iter_Schm);
 
       elsif Nkind (I) = N_Subtype_Indication then
 
@@ -15965,7 +16629,8 @@ package body Sem_Ch3 is
          R := Range_Expression (Constraint (I));
 
          Resolve (R, T);
-         Process_Range_Expr_In_Decl (R, Entity (Subtype_Mark (I)));
+         Process_Range_Expr_In_Decl
+           (R, Entity (Subtype_Mark (I)), In_Iter_Schm => In_Iter_Schm);
 
       elsif Nkind (I) = N_Attribute_Reference then
 
@@ -16151,6 +16816,21 @@ package body Sem_Ch3 is
    --  Start of processing for Modular_Type_Declaration
 
    begin
+      --  If the mod expression is (exactly) 2 * literal, where literal is
+      --  64 or less,then almost certainly the * was meant to be **. Warn!
+
+      if Warn_On_Suspicious_Modulus_Value
+        and then Nkind (Mod_Expr) = N_Op_Multiply
+        and then Nkind (Left_Opnd (Mod_Expr)) = N_Integer_Literal
+        and then Intval (Left_Opnd (Mod_Expr)) = Uint_2
+        and then Nkind (Right_Opnd (Mod_Expr)) = N_Integer_Literal
+        and then Intval (Right_Opnd (Mod_Expr)) <= Uint_64
+      then
+         Error_Msg_N ("suspicious MOD value, was '*'* intended'??", Mod_Expr);
+      end if;
+
+      --  Proceed with analysis of mod expression
+
       Analyze_And_Resolve (Mod_Expr, Any_Integer);
       Set_Etype (T, T);
       Set_Ekind (T, E_Modular_Integer_Type);
@@ -16202,6 +16882,7 @@ package body Sem_Ch3 is
          --  Non-binary case
 
          elsif M_Val < 2 ** Bits then
+            Check_SPARK_Restriction ("modulus should be a power of 2", T);
             Set_Non_Binary_Modulus (T);
 
             if Bits > System_Max_Nonbinary_Modulus_Power then
@@ -16320,12 +17001,17 @@ package body Sem_Ch3 is
       --  function calls. The function call may have been given in prefixed
       --  notation, in which case the original node is an indexed component.
       --  If the function is parameterless, the original node was an explicit
-      --  dereference.
+      --  dereference. The function may also be parameterless, in which case
+      --  the source node is just an identifier.
 
       case Nkind (Original_Node (Exp)) is
          when N_Aggregate | N_Extension_Aggregate | N_Function_Call | N_Op =>
             return True;
 
+         when N_Identifier =>
+            return Present (Entity (Original_Node (Exp)))
+              and then Ekind (Entity (Original_Node (Exp))) = E_Function;
+
          when N_Qualified_Expression =>
             return
               OK_For_Limited_Init_In_05
@@ -16358,6 +17044,36 @@ package body Sem_Ch3 is
          when N_Attribute_Reference =>
             return Attribute_Name (Original_Node (Exp)) = Name_Input;
 
+         --  For a conditional expression, all dependent expressions must be
+         --  legal constructs.
+
+         when N_Conditional_Expression =>
+            declare
+               Then_Expr : constant Node_Id :=
+                             Next (First (Expressions (Original_Node (Exp))));
+               Else_Expr : constant Node_Id := Next (Then_Expr);
+            begin
+               return OK_For_Limited_Init_In_05 (Typ, Then_Expr)
+                 and then OK_For_Limited_Init_In_05 (Typ, Else_Expr);
+            end;
+
+         when N_Case_Expression =>
+            declare
+               Alt : Node_Id;
+
+            begin
+               Alt := First (Alternatives (Original_Node (Exp)));
+               while Present (Alt) loop
+                  if not OK_For_Limited_Init_In_05 (Typ, Expression (Alt)) then
+                     return False;
+                  end if;
+
+                  Next (Alt);
+               end loop;
+
+               return True;
+            end;
+
          when others =>
             return False;
       end case;
@@ -16720,9 +17436,8 @@ package body Sem_Ch3 is
             --  worst, and therefore defaults are not allowed if the parent is
             --  a generic formal private type (see ACATS B370001).
 
-            if Is_Access_Type (Discr_Type) then
+            if Is_Access_Type (Discr_Type) and then Default_Present then
                if Ekind (Discr_Type) /= E_Anonymous_Access_Type
-                 or else not Default_Present
                  or else Is_Limited_Record (Current_Scope)
                  or else Is_Concurrent_Type (Current_Scope)
                  or else Is_Concurrent_Record_Type (Current_Scope)
@@ -16925,9 +17640,13 @@ package body Sem_Ch3 is
         and then (Is_Limited_Type (Full_T)
                    or else Is_Limited_Composite (Full_T))
       then
-         Error_Msg_N
-           ("completion of nonlimited type cannot be limited", Full_T);
-         Explain_Limited_Type (Full_T, Full_T);
+         if In_Instance then
+            null;
+         else
+            Error_Msg_N
+              ("completion of nonlimited type cannot be limited", Full_T);
+            Explain_Limited_Type (Full_T, Full_T);
+         end if;
 
       elsif Is_Abstract_Type (Full_T)
         and then not Is_Abstract_Type (Priv_T)
@@ -16946,10 +17665,11 @@ package body Sem_Ch3 is
             Set_Is_Limited_Record (Full_T);
 
          --  GNAT allow its own definition of Limited_Controlled to disobey
-         --  this rule in order in ease the implementation. The next test is
-         --  safe because Root_Controlled is defined in a private system child
+         --  this rule in order in ease the implementation. This test is safe
+         --  because Root_Controlled is defined in a child of System that
+         --  normal programs are not supposed to use.
 
-         elsif Etype (Full_T) = Full_View (RTE (RE_Root_Controlled)) then
+         elsif Is_RTE (Etype (Full_T), RE_Root_Controlled) then
             Set_Is_Limited_Composite (Full_T);
          else
             Error_Msg_N
@@ -16980,7 +17700,7 @@ package body Sem_Ch3 is
 
             --  Ada 2005 (AI-251): The partial view shall be a descendant of
             --  an interface type if and only if the full type is descendant
-            --  of the interface type (AARM 7.3 (7.3/2).
+            --  of the interface type (AARM 7.3 (7.3/2)).
 
             Iface := Find_Hidden_Interface (Priv_T_Ifaces, Full_T_Ifaces);
 
@@ -17047,89 +17767,108 @@ package body Sem_Ch3 is
               ("parent of full type must descend from parent"
                   & " of private extension", Full_Indic);
 
-         --  Check the rules of 7.3(10): if the private extension inherits
-         --  known discriminants, then the full type must also inherit those
-         --  discriminants from the same (ancestor) type, and the parent
-         --  subtype of the full type must be constrained if and only if
-         --  the ancestor subtype of the private extension is constrained.
+         --  First check a formal restriction, and then proceed with checking
+         --  Ada rules. Since the formal restriction is not a serious error, we
+         --  don't prevent further error detection for this check, hence the
+         --  ELSE.
 
-         elsif No (Discriminant_Specifications (Parent (Priv_T)))
-           and then not Has_Unknown_Discriminants (Priv_T)
-           and then Has_Discriminants (Base_Type (Priv_Parent))
-         then
-            declare
-               Priv_Indic  : constant Node_Id :=
-                               Subtype_Indication (Parent (Priv_T));
+         else
 
-               Priv_Constr : constant Boolean :=
-                               Is_Constrained (Priv_Parent)
-                                 or else
-                                   Nkind (Priv_Indic) = N_Subtype_Indication
-                                 or else Is_Constrained (Entity (Priv_Indic));
+            --  In formal mode, when completing a private extension the type
+            --  named in the private part must be exactly the same as that
+            --  named in the visible part.
 
-               Full_Constr : constant Boolean :=
-                               Is_Constrained (Full_Parent)
-                                 or else
-                                   Nkind (Full_Indic) = N_Subtype_Indication
-                                 or else Is_Constrained (Entity (Full_Indic));
+            if Priv_Parent /= Full_Parent then
+               Error_Msg_Name_1 := Chars (Priv_Parent);
+               Check_SPARK_Restriction ("% expected", Full_Indic);
+            end if;
 
-               Priv_Discr : Entity_Id;
-               Full_Discr : Entity_Id;
+            --  Check the rules of 7.3(10): if the private extension inherits
+            --  known discriminants, then the full type must also inherit those
+            --  discriminants from the same (ancestor) type, and the parent
+            --  subtype of the full type must be constrained if and only if
+            --  the ancestor subtype of the private extension is constrained.
 
-            begin
-               Priv_Discr := First_Discriminant (Priv_Parent);
-               Full_Discr := First_Discriminant (Full_Parent);
-               while Present (Priv_Discr) and then Present (Full_Discr) loop
-                  if Original_Record_Component (Priv_Discr) =
-                     Original_Record_Component (Full_Discr)
-                    or else
-                     Corresponding_Discriminant (Priv_Discr) =
-                     Corresponding_Discriminant (Full_Discr)
-                  then
-                     null;
-                  else
-                     exit;
-                  end if;
+            if No (Discriminant_Specifications (Parent (Priv_T)))
+              and then not Has_Unknown_Discriminants (Priv_T)
+              and then Has_Discriminants (Base_Type (Priv_Parent))
+            then
+               declare
+                  Priv_Indic  : constant Node_Id :=
+                                  Subtype_Indication (Parent (Priv_T));
+
+                  Priv_Constr : constant Boolean :=
+                                  Is_Constrained (Priv_Parent)
+                                    or else
+                                      Nkind (Priv_Indic) = N_Subtype_Indication
+                                    or else
+                                      Is_Constrained (Entity (Priv_Indic));
+
+                  Full_Constr : constant Boolean :=
+                                  Is_Constrained (Full_Parent)
+                                    or else
+                                      Nkind (Full_Indic) = N_Subtype_Indication
+                                    or else
+                                      Is_Constrained (Entity (Full_Indic));
+
+                  Priv_Discr : Entity_Id;
+                  Full_Discr : Entity_Id;
 
-                  Next_Discriminant (Priv_Discr);
-                  Next_Discriminant (Full_Discr);
-               end loop;
+               begin
+                  Priv_Discr := First_Discriminant (Priv_Parent);
+                  Full_Discr := First_Discriminant (Full_Parent);
+                  while Present (Priv_Discr) and then Present (Full_Discr) loop
+                     if Original_Record_Component (Priv_Discr) =
+                        Original_Record_Component (Full_Discr)
+                       or else
+                         Corresponding_Discriminant (Priv_Discr) =
+                         Corresponding_Discriminant (Full_Discr)
+                     then
+                        null;
+                     else
+                        exit;
+                     end if;
 
-               if Present (Priv_Discr) or else Present (Full_Discr) then
-                  Error_Msg_N
-                    ("full view must inherit discriminants of the parent type"
-                     & " used in the private extension", Full_Indic);
+                     Next_Discriminant (Priv_Discr);
+                     Next_Discriminant (Full_Discr);
+                  end loop;
 
-               elsif Priv_Constr and then not Full_Constr then
-                  Error_Msg_N
-                    ("parent subtype of full type must be constrained",
-                     Full_Indic);
+                  if Present (Priv_Discr) or else Present (Full_Discr) then
+                     Error_Msg_N
+                       ("full view must inherit discriminants of the parent"
+                        & " type used in the private extension", Full_Indic);
 
-               elsif Full_Constr and then not Priv_Constr then
-                  Error_Msg_N
-                    ("parent subtype of full type must be unconstrained",
-                     Full_Indic);
-               end if;
-            end;
+                  elsif Priv_Constr and then not Full_Constr then
+                     Error_Msg_N
+                       ("parent subtype of full type must be constrained",
+                        Full_Indic);
+
+                  elsif Full_Constr and then not Priv_Constr then
+                     Error_Msg_N
+                       ("parent subtype of full type must be unconstrained",
+                        Full_Indic);
+                  end if;
+               end;
 
-         --  Check the rules of 7.3(12): if a partial view has neither known
-         --  or unknown discriminants, then the full type declaration shall
-         --  define a definite subtype.
+               --  Check the rules of 7.3(12): if a partial view has neither
+               --  known or unknown discriminants, then the full type
+               --  declaration shall define a definite subtype.
 
-         elsif      not Has_Unknown_Discriminants (Priv_T)
-           and then not Has_Discriminants (Priv_T)
-           and then not Is_Constrained (Full_T)
-         then
-            Error_Msg_N
-              ("full view must define a constrained type if partial view"
-                & " has no discriminants", Full_T);
-         end if;
+            elsif      not Has_Unknown_Discriminants (Priv_T)
+              and then not Has_Discriminants (Priv_T)
+              and then not Is_Constrained (Full_T)
+            then
+               Error_Msg_N
+                 ("full view must define a constrained type if partial view"
+                  & " has no discriminants", Full_T);
+            end if;
 
-         --  ??????? Do we implement the following properly ?????
-         --  If the ancestor subtype of a private extension has constrained
-         --  discriminants, then the parent subtype of the full view shall
-         --  impose a statically matching constraint on those discriminants
-         --  [7.3(13)].
+            --  ??????? Do we implement the following properly ?????
+            --  If the ancestor subtype of a private extension has constrained
+            --  discriminants, then the parent subtype of the full view shall
+            --  impose a statically matching constraint on those discriminants
+            --  [7.3(13)].
+         end if;
 
       else
          --  For untagged types, verify that a type without discriminants
@@ -17421,6 +18160,11 @@ package body Sem_Ch3 is
       if Is_CPP_Class (Priv_T) then
          Set_Is_CPP_Class (Full_T);
          Set_Convention   (Full_T, Convention_CPP);
+
+         --  Check that components of imported CPP types do not have default
+         --  expressions.
+
+         Check_CPP_Type_Has_No_Defaults (Full_T);
       end if;
 
       --  If the private view has user specified stream attributes, then so has
@@ -17459,7 +18203,7 @@ package body Sem_Ch3 is
 
       if Has_Predicates (Priv_T) then
          Set_Predicate_Function (Priv_T, Predicate_Function (Full_T));
-         Set_Has_Predicates (Priv_T);
+         Set_Has_Predicates (Full_T);
       end if;
    end Process_Full_View;
 
@@ -17516,17 +18260,17 @@ package body Sem_Ch3 is
 
          elsif Is_Overloadable (Priv_Dep) then
 
-            --  A protected operation is never dispatching: only its
-            --  wrapper operation (which has convention Ada) is.
+            --  If a subprogram in the incomplete dependents list is primitive
+            --  for a tagged full type then mark it as a dispatching operation,
+            --  check whether it overrides an inherited subprogram, and check
+            --  restrictions on its controlling formals. Note that a protected
+            --  operation is never dispatching: only its wrapper operation
+            --  (which has convention Ada) is.
 
             if Is_Tagged_Type (Full_T)
+              and then Is_Primitive (Priv_Dep)
               and then Convention (Priv_Dep) /= Convention_Protected
             then
-
-               --  Subprogram has an access parameter whose designated type
-               --  was incomplete. Reexamine declaration now, because it may
-               --  be a primitive operation of the full type.
-
                Check_Operation_From_Incomplete_Type (Priv_Dep, Inc_T);
                Set_Is_Dispatching_Operation (Priv_Dep);
                Check_Controlling_Formals (Full_T, Priv_Dep);
@@ -17584,10 +18328,11 @@ package body Sem_Ch3 is
    --------------------------------
 
    procedure Process_Range_Expr_In_Decl
-     (R           : Node_Id;
-      T           : Entity_Id;
-      Check_List  : List_Id := Empty_List;
-      R_Check_Off : Boolean := False)
+     (R            : Node_Id;
+      T            : Entity_Id;
+      Check_List   : List_Id := Empty_List;
+      R_Check_Off  : Boolean := False;
+      In_Iter_Schm : Boolean := False)
    is
       Lo, Hi      : Node_Id;
       R_Checks    : Check_Result;
@@ -17598,6 +18343,16 @@ package body Sem_Ch3 is
       Analyze_And_Resolve (R, Base_Type (T));
 
       if Nkind (R) = N_Range then
+
+         --  In SPARK, all ranges should be static, with the exception of the
+         --  discrete type definition of a loop parameter specification.
+
+         if not In_Iter_Schm
+           and then not Is_Static_Range (R)
+         then
+            Check_SPARK_Restriction ("range should be static", R);
+         end if;
+
          Lo := Low_Bound (R);
          Hi := High_Bound (R);
 
@@ -17688,6 +18443,11 @@ package body Sem_Ch3 is
             --  if needed, before applying checks, since checks may cause
             --  duplication of the expression without forcing evaluation.
 
+            --  The forced evaluation removes side effects from expressions,
+            --  which should occur also in Alfa mode. Otherwise, we end up with
+            --  unexpected insertions of actions at places where this is not
+            --  supposed to occur, e.g. on default parameters of a call.
+
             if Expander_Active then
                Force_Evaluation (Lo);
                Force_Evaluation (Hi);
@@ -17702,7 +18462,7 @@ package body Sem_Ch3 is
 
                --  Look up tree to find an appropriate insertion point. We
                --  can't just use insert_actions because later processing
-               --  depends on the insertion node. Prior to Ada2012 the
+               --  depends on the insertion node. Prior to Ada 2012 the
                --  insertion point could only be a declaration or a loop, but
                --  quantified expressions can appear within any context in an
                --  expression, and the insertion point can be any statement,
@@ -17798,6 +18558,11 @@ package body Sem_Ch3 is
 
       --  Case of other than an explicit N_Range node
 
+      --  The forced evaluation removes side effects from expressions, which
+      --  should occur also in Alfa mode. Otherwise, we end up with unexpected
+      --  insertions of actions at places where this is not supposed to occur,
+      --  e.g. on default parameters of a call.
+
       elsif Expander_Active then
          Get_Index_Bounds (R, Lo, Hi);
          Force_Evaluation (Lo);
@@ -18068,9 +18833,11 @@ package body Sem_Ch3 is
             return Process_Subtype (S, Related_Nod, Related_Id, Suffix);
          end if;
 
-         --  Remaining processing depends on type
+         --  Remaining processing depends on type. Select on Base_Type kind to
+         --  ensure getting to the concrete type kind in the case of a private
+         --  subtype (needed when only doing semantic analysis).
 
-         case Ekind (Subtype_Mark_Id) is
+         case Ekind (Base_Type (Subtype_Mark_Id)) is
             when Access_Kind =>
                Constrain_Access (Def_Id, S, Related_Nod);
 
@@ -18475,7 +19242,7 @@ package body Sem_Ch3 is
             --  an access_to_object or an access_to_subprogram.
 
             if Present (Acc_Def) then
-               if Nkind  (Acc_Def) = N_Access_Function_Definition then
+               if Nkind (Acc_Def) = N_Access_Function_Definition then
                   Type_Def :=
                     Make_Access_Function_Definition (Loc,
                       Parameter_Specifications =>
@@ -18514,10 +19281,15 @@ package body Sem_Ch3 is
             Insert_Before (Typ_Decl, Decl);
             Analyze (Decl);
 
-            --  If an access to object, Preserve entity of designated type,
+            --  If an access to subprogram, create the extra formals
+
+            if Present (Acc_Def) then
+               Create_Extra_Formals (Designated_Type (Anon_Access));
+
+            --  If an access to object, preserve entity of designated type,
             --  for ASIS use, before rewriting the component definition.
 
-            if No (Acc_Def) then
+            else
                declare
                   Desig : Entity_Id;
 
@@ -18608,6 +19380,14 @@ package body Sem_Ch3 is
       if Ada_Version < Ada_2005
         or else not Interface_Present (Def)
       then
+         if Limited_Present (Def) then
+            Check_SPARK_Restriction ("limited is not allowed", N);
+         end if;
+
+         if Abstract_Present (Def) then
+            Check_SPARK_Restriction ("abstract is not allowed", N);
+         end if;
+
          --  The flag Is_Tagged_Type might have already been set by
          --  Find_Type_Name if it detected an error for declaration T. This
          --  arises in the case of private tagged types where the full view
@@ -18627,6 +19407,8 @@ package body Sem_Ch3 is
                                       or else Abstract_Present (Def));
 
       else
+         Check_SPARK_Restriction ("interface is not allowed", N);
+
          Is_Tagged := True;
          Analyze_Interface_Declaration (T, Def);
 
@@ -18765,6 +19547,40 @@ package body Sem_Ch3 is
          T := Prev_T;
       end if;
 
+      --  In SPARK, tagged types and type extensions may only be declared in
+      --  the specification of library unit packages.
+
+      if Present (Def) and then Is_Tagged_Type (T) then
+         declare
+            Typ  : Node_Id;
+            Ctxt : Node_Id;
+
+         begin
+            if Nkind (Parent (Def)) = N_Full_Type_Declaration then
+               Typ := Parent (Def);
+            else
+               pragma Assert
+                 (Nkind (Parent (Def)) = N_Derived_Type_Definition);
+               Typ := Parent (Parent (Def));
+            end if;
+
+            Ctxt := Parent (Typ);
+
+            if Nkind (Ctxt) = N_Package_Body
+              and then Nkind (Parent (Ctxt)) = N_Compilation_Unit
+            then
+               Check_SPARK_Restriction
+                 ("type should be defined in package specification", Typ);
+
+            elsif Nkind (Ctxt) /= N_Package_Specification
+              or else Nkind (Parent (Parent (Ctxt))) /= N_Compilation_Unit
+            then
+               Check_SPARK_Restriction
+                 ("type should be defined in library unit package", Typ);
+            end if;
+         end;
+      end if;
+
       Final_Storage_Only := not Is_Controlled (T);
 
       --  Ada 2005: check whether an explicit Limited is present in a derived
@@ -18787,12 +19603,15 @@ package body Sem_Ch3 is
         or else No (Component_List (Def))
         or else Null_Present (Component_List (Def))
       then
-         null;
+         if not Is_Tagged_Type (T) then
+            Check_SPARK_Restriction ("non-tagged record cannot be null", Def);
+         end if;
 
       else
          Analyze_Declarations (Component_Items (Component_List (Def)));
 
          if Present (Variant_Part (Component_List (Def))) then
+            Check_SPARK_Restriction ("variant part is not allowed", Def);
             Analyze (Variant_Part (Component_List (Def)));
          end if;
       end if;
@@ -18922,17 +19741,16 @@ package body Sem_Ch3 is
    --  do not know the exact end points at the time of the declaration. This
    --  is true for three reasons:
 
-   --     A size clause may affect the fudging of the end-points
-   --     A small clause may affect the values of the end-points
-   --     We try to include the end-points if it does not affect the size
-
-   --  This means that the actual end-points must be established at the point
-   --  when the type is frozen. Meanwhile, we first narrow the range as
-   --  permitted (so that it will fit if necessary in a small specified size),
-   --  and then build a range subtree with these narrowed bounds.
+   --     A size clause may affect the fudging of the end-points.
+   --     A small clause may affect the values of the end-points.
+   --     We try to include the end-points if it does not affect the size.
 
-   --  Set_Fixed_Range constructs the range from real literal values, and sets
-   --  the range as the Scalar_Range of the given fixed-point type entity.
+   --  This means that the actual end-points must be established at the
+   --  point when the type is frozen. Meanwhile, we first narrow the range
+   --  as permitted (so that it will fit if necessary in a small specified
+   --  size), and then build a range subtree with these narrowed bounds.
+   --  Set_Fixed_Range constructs the range from real literal values, and
+   --  sets the range as the Scalar_Range of the given fixed-point type entity.
 
    --  The parent of this range is set to point to the entity so that it is
    --  properly hooked into the tree (unlike normal Scalar_Range entries for
@@ -18957,6 +19775,12 @@ package body Sem_Ch3 is
    begin
       Set_Scalar_Range (E, S);
       Set_Parent (S, E);
+
+      --  Before the freeze point, the bounds of a fixed point are universal
+      --  and carry the corresponding type.
+
+      Set_Etype (Low_Bound (S),  Universal_Real);
+      Set_Etype (High_Bound (S), Universal_Real);
    end Set_Fixed_Range;
 
    ----------------------------------
@@ -19153,7 +19977,6 @@ package body Sem_Ch3 is
       --  Complete both implicit base and declared first subtype entities
 
       Set_Etype          (Implicit_Base, Base_Typ);
-      Set_Scalar_Range   (Implicit_Base, Scalar_Range   (Base_Typ));
       Set_Size_Info      (Implicit_Base,                (Base_Typ));
       Set_RM_Size        (Implicit_Base, RM_Size        (Base_Typ));
       Set_First_Rep_Item (Implicit_Base, First_Rep_Item (Base_Typ));
@@ -19161,6 +19984,66 @@ package body Sem_Ch3 is
       Set_Ekind          (T, E_Signed_Integer_Subtype);
       Set_Etype          (T, Implicit_Base);
 
+      --  In formal verification mode, restrict the base type's range to the
+      --  minimum allowed by RM 3.5.4, namely the smallest symmetric range
+      --  around zero with a possible extra negative value that contains the
+      --  subtype range. Keep Size, RM_Size and First_Rep_Item info, which
+      --  should not be relied upon in formal verification.
+
+      if Strict_Alfa_Mode then
+         declare
+            Sym_Hi_Val : Uint;
+            Sym_Lo_Val : Uint;
+            Dloc       : constant Source_Ptr := Sloc (Def);
+            Lbound     : Node_Id;
+            Ubound     : Node_Id;
+            Bounds     : Node_Id;
+
+         begin
+            --  If the subtype range is empty, the smallest base type range
+            --  is the symmetric range around zero containing Lo_Val and
+            --  Hi_Val.
+
+            if UI_Gt (Lo_Val, Hi_Val) then
+               Sym_Hi_Val := UI_Max (UI_Abs (Lo_Val), UI_Abs (Hi_Val));
+               Sym_Lo_Val := UI_Negate (Sym_Hi_Val);
+
+               --  Otherwise, if the subtype range is not empty and Hi_Val has
+               --  the largest absolute value, Hi_Val is non negative and the
+               --  smallest base type range is the symmetric range around zero
+               --  containing Hi_Val.
+
+            elsif UI_Le (UI_Abs (Lo_Val), UI_Abs (Hi_Val)) then
+               Sym_Hi_Val := Hi_Val;
+               Sym_Lo_Val := UI_Negate (Hi_Val);
+
+               --  Otherwise, the subtype range is not empty, Lo_Val has the
+               --  strictly largest absolute value, Lo_Val is negative and the
+               --  smallest base type range is the symmetric range around zero
+               --  with an extra negative value Lo_Val.
+
+            else
+               Sym_Lo_Val := Lo_Val;
+               Sym_Hi_Val := UI_Sub (UI_Negate (Lo_Val), Uint_1);
+            end if;
+
+            Lbound := Make_Integer_Literal (Dloc, Sym_Lo_Val);
+            Ubound := Make_Integer_Literal (Dloc, Sym_Hi_Val);
+            Set_Is_Static_Expression (Lbound);
+            Set_Is_Static_Expression (Ubound);
+            Analyze_And_Resolve (Lbound, Any_Integer);
+            Analyze_And_Resolve (Ubound, Any_Integer);
+
+            Bounds := Make_Range (Dloc, Lbound, Ubound);
+            Set_Etype (Bounds, Base_Typ);
+
+            Set_Scalar_Range (Implicit_Base, Bounds);
+         end;
+
+      else
+         Set_Scalar_Range (Implicit_Base, Scalar_Range (Base_Typ));
+      end if;
+
       Set_Size_Info      (T,                (Implicit_Base));
       Set_First_Rep_Item (T, First_Rep_Item (Implicit_Base));
       Set_Scalar_Range   (T, Def);