OSDN Git Service

2011-08-05 Javier Miranda <miranda@adacore.com>
[pf3gnuchains/gcc-fork.git] / gcc / ada / sem_ch3.adb
index f0e4c49..c0187d7 100644 (file)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2011, 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;
@@ -446,7 +445,7 @@ package body Sem_Ch3 is
       Related_Id   : Entity_Id;
       Suffix       : Character;
       Suffix_Index : Nat);
-   --  Process an index constraint in a constrained array declaration. The
+   --  Process an index constraint in a constrained array declaration. The
    --  constraint can be a subtype name, or a range with or without an explicit
    --  subtype mark. The index is the corresponding index of the unconstrained
    --  array. The Related_Id and Suffix parameters are used to build the
@@ -585,8 +584,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
@@ -716,6 +714,8 @@ package body Sem_Ch3 is
       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
@@ -781,7 +781,7 @@ package body Sem_Ch3 is
 
       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 +793,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));
@@ -1028,6 +1035,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 +1181,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 +1286,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 +1317,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 +1353,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 Associated_Collection 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 collections.
+
+      if No (Associated_Storage_Pool (T)) then
+         Set_Associated_Collection (T, Empty);
+      end if;
 
       --  Ada 2005 (AI-231): Propagate the null-excluding and access-constant
       --  attributes
@@ -1572,6 +1611,26 @@ package body Sem_Ch3 is
 
                pragma Assert (Present (Prim));
 
+               --  Ada 2012 (AI05-0197): If the name of the covering primitive
+               --  differs from the name of the interface primitive then it is
+               --  a private primitive inherited from a parent type. In such
+               --  case, given that Tagged_Type covers the interface, the
+               --  inherited private primitive becomes visible. For such
+               --  purpose we add a new entity that renames the inherited
+               --  private primitive.
+
+               if Chars (Prim) /= Chars (Iface_Prim) then
+                  pragma Assert (Has_Suffix (Prim, 'P'));
+                  Derive_Subprogram
+                    (New_Subp     => New_Subp,
+                     Parent_Subp  => Iface_Prim,
+                     Derived_Type => Tagged_Type,
+                     Parent_Type  => Iface);
+                  Set_Alias (New_Subp, Prim);
+                  Set_Is_Abstract_Subprogram
+                    (New_Subp, Is_Abstract_Subprogram (Prim));
+               end if;
+
                Derive_Subprogram
                  (New_Subp     => New_Subp,
                   Parent_Subp  => Iface_Prim,
@@ -1626,10 +1685,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
@@ -1739,10 +1800,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
@@ -1793,6 +1858,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);
 
@@ -1954,7 +2020,10 @@ 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;
    end Analyze_Component_Declaration;
 
    --------------------------
@@ -1988,9 +2057,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);
@@ -2097,11 +2180,18 @@ 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;
+
+               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);
@@ -2126,9 +2216,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 --
@@ -2148,7 +2241,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
@@ -2206,17 +2298,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;
 
@@ -2311,6 +2409,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));
@@ -2403,8 +2507,16 @@ package body Sem_Ch3 is
       Set_Optimize_Alignment_Flags (Def_Id);
       Check_Eliminated (Def_Id);
 
-      if Nkind (N) = N_Full_Type_Declaration then
-         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;
 
@@ -2417,6 +2529,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
@@ -2457,7 +2571,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;
 
    -----------------------------------
@@ -2745,7 +2859,7 @@ 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
 
@@ -2950,6 +3064,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
@@ -2964,8 +3107,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",
@@ -3065,6 +3208,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
@@ -3079,6 +3234,27 @@ package body Sem_Ch3 is
          end if;
       end if;
 
+      --  Deal with predicate check before we start to do major rewriting.
+      --  it is OK to initialize and then check the initialized value, since
+      --  the object goes out of scope if we get a predicate failure. Note
+      --  that we do this in the analyzer and not the expander because the
+      --  analyzer does some substantial rewriting in some cases.
+
+      --  We need a predicate check if the type has predicates, and if either
+      --  there is an initializing expression, or for default initialization
+      --  when we have at least one case of an explicit default initial value.
+
+      if not Suppress_Assignment_Checks (N)
+        and then Present (Predicate_Function (T))
+        and then
+          (Present (E)
+            or else
+              Is_Partially_Initialized_Type (T, Include_Implicit => False))
+      then
+         Insert_After (N,
+           Make_Predicate_Check (T, New_Occurrence_Of (Id, Loc)));
+      end if;
+
       --  Case of unconstrained type
 
       if Is_Indefinite_Subtype (T) then
@@ -3250,15 +3426,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);
 
@@ -3272,9 +3460,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)
@@ -3547,14 +3735,17 @@ 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;
    end Analyze_Object_Declaration;
 
    ---------------------------
@@ -3692,6 +3883,15 @@ package body Sem_Ch3 is
 
       Build_Derived_Record_Type (N, Parent_Type, T);
 
+      --  Propagate inherited invariant information. The new type has
+      --  invariants, if the parent type has inheritable invariants,
+      --  and these invariants can in turn be inherited.
+
+      if Has_Inheritable_Invariants (Parent_Type) then
+         Set_Has_Inheritable_Invariants (T);
+         Set_Has_Invariants (T);
+      end if;
+
       --  Ada 2005 (AI-443): Synchronized private extension or a rewritten
       --  synchronized formal derived type.
 
@@ -3784,8 +3984,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;
 
    ---------------------------------
@@ -3823,9 +4025,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;
 
@@ -3844,7 +4046,72 @@ package body Sem_Ch3 is
       Set_Is_Ada_2005_Only  (Id, Is_Ada_2005_Only  (T));
       Set_Is_Ada_2012_Only  (Id, Is_Ada_2012_Only  (T));
       Set_Convention        (Id, Convention        (T));
-      Set_Has_Predicates    (Id, Has_Predicates    (T));
+
+      --  If ancestor has predicates then so does the subtype, and in addition
+      --  we must delay the freeze to properly arrange predicate inheritance.
+
+      --  The Ancestor_Type test is a big kludge, there seem to be cases in
+      --  which T = ID, so the above tests and assignments do nothing???
+
+      if Has_Predicates (T)
+        or else (Present (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
@@ -3853,6 +4120,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);
@@ -3938,6 +4215,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));
 
@@ -3971,6 +4250,8 @@ package body Sem_Ch3 is
                Set_Last_Entity        (Id, Last_Entity           (T));
                Set_Private_Dependents (Id, New_Elmt_List);
                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));
                Set_Known_To_Have_Preelab_Init
@@ -4149,9 +4430,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))
@@ -4163,38 +4444,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;
 
@@ -4215,8 +4527,10 @@ package body Sem_Ch3 is
       Set_Optimize_Alignment_Flags (Id);
       Check_Eliminated (Id);
 
-      <<Leave>>
-         Analyze_Aspect_Specifications (N, Id, Aspect_Specifications (N));
+   <<Leave>>
+      if Has_Aspects (N) then
+         Analyze_Aspect_Specifications (N, Id);
+      end if;
    end Analyze_Subtype_Declaration;
 
    --------------------------------
@@ -4294,13 +4608,9 @@ package body Sem_Ch3 is
       Discr_Name : Node_Id;
       Discr_Type : Entity_Id;
 
-      Case_Table     : Choice_Table_Type (1 .. Number_Of_Choices (N));
-      Last_Choice    : Nat;
       Dont_Care      : Boolean;
       Others_Present : Boolean := False;
 
-      pragma Warnings (Off, Case_Table);
-      pragma Warnings (Off, Last_Choice);
       pragma Warnings (Off, Dont_Care);
       pragma Warnings (Off, Others_Present);
       --  We don't care about the assigned values of any of these
@@ -4334,8 +4644,7 @@ package body Sem_Ch3 is
 
       --  Call the instantiated Analyze_Choices which does the rest of the work
 
-      Analyze_Choices
-        (N, Discr_Type, Case_Table, Last_Choice, Dont_Care, Others_Present);
+      Analyze_Choices (N, Discr_Type, Dont_Care, Others_Present);
    end Analyze_Variant_Part;
 
    ----------------------------
@@ -4344,6 +4653,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;
@@ -4364,7 +4674,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;
@@ -4373,6 +4683,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:
 
@@ -4426,16 +4740,27 @@ package body Sem_Ch3 is
          end if;
 
          Make_Index (Index, P, Related_Id, Nb_Index);
+
+         --  Check error of subtype with predicate for index type
+
+         Bad_Predicated_Subtype_Use
+           ("subtype& has predicate, not allowed as index subtype",
+            Index, Etype (Index));
+
+         --  Move to next index
+
          Next_Index (Index);
          Nb_Index := Nb_Index + 1;
       end loop;
 
       --  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');
+
+         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
 
@@ -4543,6 +4868,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;
 
@@ -5021,33 +5348,35 @@ package body Sem_Ch3 is
          end loop;
       end if;
 
-      if Present (Old_Disc) then
+      if Present (Old_Disc) and then Expander_Active then
 
          --  The new type has fewer discriminants, so we need to create a new
          --  corresponding record, which is derived from the corresponding
          --  record of the parent, and has a stored constraint that captures
-         --  the values of the discriminant constraints.
+         --  the values of the discriminant constraints. The corresponding
+         --  record is needed only if expander is active and code generation is
+         --  enabled.
 
-         --  The type declaration for the derived corresponding record has
-         --  the same discriminant part and constraints as the current
-         --  declaration. Copy the unanalyzed tree to build declaration.
+         --  The type declaration for the derived corresponding record has the
+         --  same discriminant part and constraints as the current declaration.
+         --  Copy the unanalyzed tree to build declaration.
 
          Corr_Decl_Needed := True;
          New_N := Copy_Separate_Tree (N);
 
          Corr_Decl :=
            Make_Full_Type_Declaration (Loc,
-             Defining_Identifier => Corr_Record,
+             Defining_Identifier         => Corr_Record,
              Discriminant_Specifications =>
                 Discriminant_Specifications (New_N),
-             Type_Definition =>
+             Type_Definition             =>
                Make_Derived_Type_Definition (Loc,
                  Subtype_Indication =>
                    Make_Subtype_Indication (Loc,
                      Subtype_Mark =>
                         New_Occurrence_Of
                           (Corresponding_Record_Type (Parent_Type), Loc),
-                     Constraint =>
+                     Constraint   =>
                        Constraint
                          (Subtype_Indication (Type_Definition (New_N))))));
       end if;
@@ -5084,7 +5413,7 @@ package body Sem_Ch3 is
             Loc  : constant Source_Ptr := Sloc (N);
             Anon : constant Entity_Id :=
                      Make_Defining_Identifier (Loc,
-                       New_External_Name (Chars (Derived_Type), 'T'));
+                       Chars => New_External_Name (Chars (Derived_Type), 'T'));
             Decl : Node_Id;
 
          begin
@@ -5383,7 +5712,7 @@ package body Sem_Ch3 is
 
          Implicit_Base :=
            Make_Defining_Identifier (Sloc (Derived_Type),
-             New_External_Name (Chars (Derived_Type), 'B'));
+             Chars => New_External_Name (Chars (Derived_Type), 'B'));
 
          --  Indicate the proper nature of the derived type. This must be done
          --  before analysis of the literals, to recognize cases when a literal
@@ -5637,7 +5966,7 @@ package body Sem_Ch3 is
          --  already have been set if there was a constraint present.
 
          Set_Digits_Value (Implicit_Base, Digits_Value (Parent_Base));
-         Set_Vax_Float    (Implicit_Base, Vax_Float    (Parent_Base));
+         Set_Float_Rep    (Implicit_Base, Float_Rep    (Parent_Base));
 
          if No_Constraint then
             Set_Digits_Value (Derived_Type, Digits_Value (Parent_Type));
@@ -6035,8 +6364,9 @@ package body Sem_Ch3 is
          if not Is_Private_Type (Full_View (Parent_Type))
            and then (In_Open_Scopes (Scope (Parent_Type)))
          then
-            Full_Der := Make_Defining_Identifier (Sloc (Derived_Type),
-                                              Chars (Derived_Type));
+            Full_Der :=
+              Make_Defining_Identifier
+                (Sloc (Derived_Type), Chars (Derived_Type));
             Set_Is_Itype (Full_Der);
             Set_Has_Private_Declaration (Full_Der);
             Set_Has_Private_Declaration (Derived_Type);
@@ -6108,8 +6438,8 @@ package body Sem_Ch3 is
            and then not Is_Completion
          then
             Full_Der :=
-              Make_Defining_Identifier (Sloc (Derived_Type),
-                Chars => Chars (Derived_Type));
+              Make_Defining_Identifier
+                (Sloc (Derived_Type), Chars (Derived_Type));
             Set_Is_Itype (Full_Der);
             Set_Has_Private_Declaration (Full_Der);
             Set_Has_Private_Declaration (Derived_Type);
@@ -6182,8 +6512,8 @@ package body Sem_Ch3 is
             --  will be installed when the enclosing child body is compiled.
 
             Full_Der :=
-              Make_Defining_Identifier (Sloc (Derived_Type),
-                Chars => Chars (Derived_Type));
+              Make_Defining_Identifier
+                (Sloc (Derived_Type), Chars (Derived_Type));
             Set_Is_Itype (Full_Der);
             Build_Itype_Reference (Full_Der, N);
 
@@ -6650,35 +6980,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
@@ -6690,6 +7017,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
@@ -6918,14 +7267,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
@@ -7526,6 +7879,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
@@ -7657,18 +8012,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.
@@ -7811,9 +8171,7 @@ package body Sem_Ch3 is
    begin
       --  A discriminal has the same name as the discriminant
 
-      D_Minal :=
-        Make_Defining_Identifier (Sloc (Discrim),
-          Chars => Chars (Discrim));
+      D_Minal := Make_Defining_Identifier (Sloc (Discrim), Chars (Discrim));
 
       Set_Ekind     (D_Minal, E_In_Parameter);
       Set_Mechanism (D_Minal, Default_Mechanism);
@@ -7987,7 +8345,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;
 
@@ -8006,14 +8366,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;
@@ -8235,6 +8592,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
@@ -8247,7 +8606,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;
 
@@ -8318,8 +8677,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;
 
    ------------------------
@@ -8615,10 +8981,9 @@ package body Sem_Ch3 is
                    New_Reference_To (Subp, Loc)),
 
                Make_Pragma_Argument_Association (Loc,
-                 Expression =>
-                   Make_Identifier (Loc, Iface_Kind))));
+                 Expression => Make_Identifier (Loc, Iface_Kind))));
 
-         --  The pragma doesn't need to be analyzed because it is internaly
+         --  The pragma doesn't need to be analyzed because it is internally
          --  build. It is safe to directly register it as a rep item since we
          --  are only interested in the characters of the implementation kind.
 
@@ -8761,9 +9126,22 @@ package body Sem_Ch3 is
                            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;
@@ -8857,7 +9235,6 @@ package body Sem_Ch3 is
          --  primitive marked with pragma Implemented.
 
          if Ada_Version >= Ada_2012
-           and then Is_Overriding_Operation (Subp)
            and then Present (Overridden_Operation (Subp))
            and then Has_Rep_Pragma
                       (Overridden_Operation (Subp), Name_Implemented)
@@ -9630,16 +10007,28 @@ package body Sem_Ch3 is
 
                --  Handle the case where there is an untagged partial view and
                --  the full view is tagged: must disallow discriminants with
-               --  defaults. However suppress the error here if it was already
-               --  reported on the default expression of the partial view.
+               --  defaults, unless compiling for Ada 2012, which allows a
+               --  limited tagged type to have defaulted discriminants (see
+               --  AI05-0214). However, suppress the error here if it was
+               --  already reported on the default expression of the partial
+               --  view.
 
                if Is_Tagged_Type (T)
                     and then Present (Expression (Parent (D)))
+                    and then (not Is_Limited_Type (Current_Scope)
+                               or else Ada_Version < Ada_2012)
                     and then not Error_Posted (Expression (Parent (D)))
                then
-                  Error_Msg_N
-                    ("discriminants of tagged type cannot have defaults",
-                     Expression (New_D));
+                  if Ada_Version >= Ada_2012 then
+                     Error_Msg_N
+                       ("discriminants of nonlimited tagged type cannot have"
+                          & " defaults",
+                        Expression (New_D));
+                  else
+                     Error_Msg_N
+                       ("discriminants of tagged type cannot have defaults",
+                        Expression (New_D));
+                  end if;
                end if;
 
                --  Ada 2005 (AI-230): Access discriminant allowed in
@@ -9739,9 +10128,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:
@@ -9904,6 +10294,51 @@ package body Sem_Ch3 is
               Corresponding_Record_Type (Full_Base));
          end if;
       end if;
+
+      --  Link rep item chain, and also setting of Has_Predicates from private
+      --  subtype to full subtype, since we will need these on the full subtype
+      --  to create the predicate function. Note that the full subtype may
+      --  already have rep items, inherited from the full view of the base
+      --  type, so we must be sure not to overwrite these entries.
+
+      declare
+         Item      : Node_Id;
+         Next_Item : Node_Id;
+
+      begin
+         Item := First_Rep_Item (Full);
+
+         --  If no existing rep items on full type, we can just link directly
+         --  to the list of items on the private type.
+
+         if No (Item) then
+            Set_First_Rep_Item (Full, First_Rep_Item (Priv));
+
+         --  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
+            loop
+               Next_Item := Next_Rep_Item (Item);
+               exit when No (Next_Item);
+               Item := Next_Item;
+            end loop;
+
+            --  And link the private type items at the end of the chain
+
+            Set_Next_Rep_Item (Item, First_Rep_Item (Priv));
+         end if;
+      end;
+
+      --  Make sure Has_Predicates is set on full type if it is set on the
+      --  private type. Note that it may already be set on the full type and
+      --  if so, we don't want to unset it.
+
+      if Has_Predicates (Priv) then
+         Set_Has_Predicates (Full);
+      end if;
    end Complete_Private_Subtype;
 
    ----------------------------
@@ -10317,7 +10752,7 @@ package body Sem_Ch3 is
                   "be allowed in Ada 2005?", S);
             else
                Error_Msg_N
-                 ("access subype of general access type not allowed", S);
+                 ("access subtype of general access type not allowed", S);
             end if;
 
             Error_Msg_N ("\discriminants have defaults", S);
@@ -10989,6 +11424,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);
 
@@ -11215,6 +11653,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
@@ -11286,7 +11726,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);
@@ -11315,6 +11755,15 @@ 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.
+
+         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
@@ -11334,6 +11783,13 @@ package body Sem_Ch3 is
 
             elsif Base_Type (Entity (S)) /= Base_Type (T) then
                Wrong_Type (S, Base_Type (T));
+
+            --  Check error of subtype with predicate in index constraint
+
+            else
+               Bad_Predicated_Subtype_Use
+                 ("subtype& has predicate, not allowed in index constraint",
+                  S, Entity (S));
             end if;
 
             return;
@@ -11419,6 +11875,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
@@ -11618,7 +12076,7 @@ package body Sem_Ch3 is
          Set_Direct_Primitive_Operations (Full,
            Direct_Primitive_Operations (Priv));
 
-         if Priv = Base_Type (Priv) then
+         if Is_Base_Type (Priv) then
             Set_Class_Wide_Type      (Full, Class_Wide_Type         (Priv));
          end if;
       end if;
@@ -11643,10 +12101,10 @@ package body Sem_Ch3 is
             Access_Types_To_Process (Freeze_Node (Priv)));
       end if;
 
-      --  Swap the two entities. Now Privat is the full type entity and Full is
-      --  the private one. They will be swapped back at the end of the private
-      --  part. This swapping ensures that the entity that is visible in the
-      --  private part is the full declaration.
+      --  Swap the two entities. Now Private is the full type entity and Full
+      --  is the private one. They will be swapped back at the end of the
+      --  private part. This swapping ensures that the entity that is visible
+      --  in the private part is the full declaration.
 
       Exchange_Entities (Priv, Full);
       Append_Entity (Full, Scope (Full));
@@ -11749,8 +12207,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)
@@ -11759,7 +12217,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;
@@ -12025,7 +12482,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;
@@ -12075,6 +12531,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
@@ -12318,6 +12776,22 @@ package body Sem_Ch3 is
                      Derive_Subprogram
                        (New_Subp, Iface_Subp, Tagged_Type, Iface);
 
+                  --  Ada 2012 (AI05-0197): If the covering primitive's name
+                  --  differs from the name of the interface primitive then it
+                  --  is a private primitive inherited from a parent type. In
+                  --  such case, given that Tagged_Type covers the interface,
+                  --  the inherited private primitive becomes visible. For such
+                  --  purpose we add a new entity that renames the inherited
+                  --  private primitive.
+
+                  elsif Chars (E) /= Chars (Iface_Subp) then
+                     pragma Assert (Has_Suffix (E, 'P'));
+                     Derive_Subprogram
+                       (New_Subp, Iface_Subp, Tagged_Type, Iface);
+                     Set_Alias (New_Subp, E);
+                     Set_Is_Abstract_Subprogram (New_Subp,
+                       Is_Abstract_Subprogram (E));
+
                   --  Propagate to the full view interface entities associated
                   --  with the partial view
 
@@ -12555,6 +13029,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
@@ -12877,9 +13352,18 @@ package body Sem_Ch3 is
                   Collect_Primitive_Operations (Parent_Type);
 
       function Check_Derived_Type return Boolean;
-      --  Check that all primitive inherited from Parent_Type are found in
+      --  Check that all the entities derived from Parent_Type are found in
       --  the list of primitives of Derived_Type exactly in the same order.
 
+      procedure Derive_Interface_Subprogram
+        (New_Subp    : in out Entity_Id;
+         Subp        : Entity_Id;
+         Actual_Subp : Entity_Id);
+      --  Derive New_Subp from the ultimate alias of the parent subprogram Subp
+      --  (which is an interface primitive). If Generic_Actual is present then
+      --  Actual_Subp is the actual subprogram corresponding with the generic
+      --  subprogram Subp.
+
       function Check_Derived_Type return Boolean is
          E        : Entity_Id;
          Elmt     : Elmt_Id;
@@ -12955,6 +13439,45 @@ package body Sem_Ch3 is
          return True;
       end Check_Derived_Type;
 
+      ---------------------------------
+      -- Derive_Interface_Subprogram --
+      ---------------------------------
+
+      procedure Derive_Interface_Subprogram
+        (New_Subp    : in out Entity_Id;
+         Subp        : Entity_Id;
+         Actual_Subp : Entity_Id)
+      is
+         Iface_Subp : constant Entity_Id := Ultimate_Alias (Subp);
+         Iface_Type : constant Entity_Id := Find_Dispatching_Type (Iface_Subp);
+
+      begin
+         pragma Assert (Is_Interface (Iface_Type));
+
+         Derive_Subprogram
+           (New_Subp     => New_Subp,
+            Parent_Subp  => Iface_Subp,
+            Derived_Type => Derived_Type,
+            Parent_Type  => Iface_Type,
+            Actual_Subp  => Actual_Subp);
+
+         --  Given that this new interface entity corresponds with a primitive
+         --  of the parent that was not overridden we must leave it associated
+         --  with its parent primitive to ensure that it will share the same
+         --  dispatch table slot when overridden.
+
+         if No (Actual_Subp) then
+            Set_Alias (New_Subp, Subp);
+
+         --  For instantiations this is not needed since the previous call to
+         --  Derive_Subprogram leaves the entity well decorated.
+
+         else
+            pragma Assert (Alias (New_Subp) = Actual_Subp);
+            null;
+         end if;
+      end Derive_Interface_Subprogram;
+
       --  Local variables
 
       Alias_Subp   : Entity_Id;
@@ -13107,7 +13630,7 @@ package body Sem_Ch3 is
             Alias_Subp := Ultimate_Alias (Subp);
 
             --  Do not derive internal entities of the parent that link
-            --  interface primitives and its covering primitive. These
+            --  interface primitives with their covering primitive. These
             --  entities will be added to this type when frozen.
 
             if Present (Interface_Alias (Subp)) then
@@ -13133,7 +13656,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
 
@@ -13262,15 +13786,74 @@ package body Sem_Ch3 is
                 (Nkind (Parent (Alias_Subp)) = N_Procedure_Specification
                   and then Null_Present (Parent (Alias_Subp)))
             then
-               Derive_Subprogram
-                 (New_Subp     => New_Subp,
-                  Parent_Subp  => Alias_Subp,
-                  Derived_Type => Derived_Type,
-                  Parent_Type  => Find_Dispatching_Type (Alias_Subp),
-                  Actual_Subp  => Act_Subp);
+               --  If this is an abstract private type then we transfer the
+               --  derivation of the interface primitive from the partial view
+               --  to the full view. This is safe because all the interfaces
+               --  must be visible in the partial view. Done to avoid adding
+               --  a new interface derivation to the private part of the
+               --  enclosing package; otherwise this new derivation would be
+               --  decorated as hidden when the analysis of the enclosing
+               --  package completes.
+
+               if Is_Abstract_Type (Derived_Type)
+                 and then In_Private_Part (Current_Scope)
+                 and then Has_Private_Declaration (Derived_Type)
+               then
+                  declare
+                     Partial_View : Entity_Id;
+                     Elmt         : Elmt_Id;
+                     Ent          : Entity_Id;
+
+                  begin
+                     Partial_View := First_Entity (Current_Scope);
+                     loop
+                        exit when No (Partial_View)
+                          or else (Has_Private_Declaration (Partial_View)
+                                     and then
+                                   Full_View (Partial_View) = Derived_Type);
+
+                        Next_Entity (Partial_View);
+                     end loop;
+
+                     --  If the partial view was not found then the source code
+                     --  has errors and the derivation is not needed.
+
+                     if Present (Partial_View) then
+                        Elmt :=
+                          First_Elmt (Primitive_Operations (Partial_View));
+                        while Present (Elmt) loop
+                           Ent := Node (Elmt);
+
+                           if Present (Alias (Ent))
+                             and then Ultimate_Alias (Ent) = Alias (Subp)
+                           then
+                              Append_Elmt
+                                (Ent, Primitive_Operations (Derived_Type));
+                              exit;
+                           end if;
+
+                           Next_Elmt (Elmt);
+                        end loop;
 
-               if No (Generic_Actual) then
-                  Set_Alias (New_Subp, Subp);
+                        --  If the interface primitive was not found in the
+                        --  partial view then this interface primitive was
+                        --  overridden. We add a derivation to activate in
+                        --  Derive_Progenitor_Subprograms the machinery to
+                        --  search for it.
+
+                        if No (Elmt) then
+                           Derive_Interface_Subprogram
+                             (New_Subp    => New_Subp,
+                              Subp        => Subp,
+                              Actual_Subp => Act_Subp);
+                        end if;
+                     end if;
+                  end;
+               else
+                  Derive_Interface_Subprogram
+                    (New_Subp     => New_Subp,
+                     Subp         => Subp,
+                     Actual_Subp  => Act_Subp);
                end if;
 
             --  Case 3: Common derivation
@@ -13445,7 +14028,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
@@ -13457,6 +14039,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);
 
@@ -13679,8 +14263,8 @@ package body Sem_Ch3 is
                           New_Copy (Subtype_Indication
                                      (Parent (Partial_View))));
 
-                        New_Iface := Make_Identifier (Sloc (N),
-                                       Chars (Parent_Type));
+                        New_Iface :=
+                          Make_Identifier (Sloc (N), Chars (Parent_Type));
                         Append (New_Iface, Interface_List (Def));
 
                         --  Analyze the transformed code
@@ -13697,17 +14281,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
@@ -13735,10 +14322,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;
@@ -13762,25 +14349,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;
 
@@ -13899,6 +14479,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;
 
    ------------------------
@@ -14239,7 +14826,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);
@@ -14533,6 +15120,19 @@ package body Sem_Ch3 is
 
       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;
@@ -14584,13 +15184,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 --
@@ -14621,6 +15227,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
@@ -14641,32 +15286,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;
+      --  Check that requested number of digits is not too high.
 
-      --  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
+         --  The check for Max_Base_Digits may be somewhat expensive, as it
+         --  requires reading System, so only do it when necessary.
 
-      else
-         Base_Typ := Standard_Long_Long_Float;
-
-         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.
@@ -14707,7 +15355,7 @@ package body Sem_Ch3 is
       Set_RM_Size        (Implicit_Base, RM_Size        (Base_Typ));
       Set_First_Rep_Item (Implicit_Base, First_Rep_Item (Base_Typ));
       Set_Digits_Value   (Implicit_Base, Digits_Value   (Base_Typ));
-      Set_Vax_Float      (Implicit_Base, Vax_Float      (Base_Typ));
+      Set_Float_Rep      (Implicit_Base, Float_Rep      (Base_Typ));
 
       Set_Ekind          (T, E_Floating_Point_Subtype);
       Set_Etype          (T, Implicit_Base);
@@ -15271,6 +15919,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 --
    -----------------------
 
@@ -15521,15 +16194,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
 
@@ -15588,7 +16277,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;
@@ -15700,7 +16390,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
 
@@ -15717,7 +16407,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
 
@@ -15929,10 +16620,8 @@ package body Sem_Ch3 is
 
       Set_Scalar_Range (T,
         Make_Range (Sloc (Mod_Expr),
-          Low_Bound  =>
-            Make_Integer_Literal (Sloc (Mod_Expr), 0),
-          High_Bound =>
-            Make_Integer_Literal (Sloc (Mod_Expr), M_Val - 1)));
+          Low_Bound  => Make_Integer_Literal (Sloc (Mod_Expr), 0),
+          High_Bound => Make_Integer_Literal (Sloc (Mod_Expr), M_Val - 1)));
 
       --  Properly analyze the literals for the range. We do this manually
       --  because we can't go calling Resolve, since we are resolving these
@@ -15956,6 +16645,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
@@ -16384,20 +17074,33 @@ package body Sem_Ch3 is
                  ("discriminant defaults not allowed for formal type",
                   Expression (Discr));
 
+            --  Flag an error for a tagged type with defaulted discriminants,
+            --  excluding limited tagged types when compiling for Ada 2012
+            --  (see AI05-0214).
+
             elsif Is_Tagged_Type (Current_Scope)
+              and then (not Is_Limited_Type (Current_Scope)
+                         or else Ada_Version < Ada_2012)
               and then Comes_From_Source (N)
             then
                --  Note: see similar test in Check_Or_Process_Discriminants, to
                --  handle the (illegal) case of the completion of an untagged
                --  view with discriminants with defaults by a tagged full view.
-               --  We skip the check if Discr does not come from source to
+               --  We skip the check if Discr does not come from source, to
                --  account for the case of an untagged derived type providing
-               --  defaults for a renamed discriminant from a private nontagged
+               --  defaults for a renamed discriminant from a private untagged
                --  ancestor with a tagged full view (ACATS B460006).
 
-               Error_Msg_N
-                 ("discriminants of tagged type cannot have defaults",
-                  Expression (Discr));
+               if Ada_Version >= Ada_2012 then
+                  Error_Msg_N
+                    ("discriminants of nonlimited tagged type cannot have"
+                       & " defaults",
+                     Expression (Discr));
+               else
+                  Error_Msg_N
+                    ("discriminants of tagged type cannot have defaults",
+                     Expression (Discr));
+               end if;
 
             else
                Default_Present := True;
@@ -16610,7 +17313,7 @@ package body Sem_Ch3 is
 
             if Ekind (Typ) = E_Record_Type_With_Private then
 
-               --  Handle the following erronous case:
+               --  Handle the following erroneous case:
                --      type Private_Type is tagged private;
                --   private
                --      type Private_Type is new Type_Implementing_Iface;
@@ -16687,10 +17390,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
@@ -16788,89 +17492,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);
 
-         --  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 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      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;
+               --  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.
 
-         --  ??????? 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)].
+            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)].
+         end if;
 
       else
          --  For untagged types, verify that a type without discriminants
@@ -17148,8 +17871,8 @@ package body Sem_Ch3 is
          --  but it means we don't have to struggle to meet the requirements in
          --  the RM for having Preelaborable Initialization. Otherwise we
          --  require that the type meets the RM rules. But we can't check that
-         --  yet, because of the rule about overriding Ininitialize, so we
-         --  simply set a flag that will be checked at freeze time.
+         --  yet, because of the rule about overriding Initialize, so we simply
+         --  set a flag that will be checked at freeze time.
 
          if not In_Predefined_Unit (Full_T) then
             Set_Must_Have_Preelab_Init (Full_T);
@@ -17185,58 +17908,15 @@ package body Sem_Ch3 is
          Set_Has_Specified_Stream_Output (Full_T);
       end if;
 
-      --  Deal with invariants
+      --  Propagate invariants to full type
 
-      if Has_Invariants (Full_T)
-           or else
-         Has_Invariants (Priv_T)
-      then
+      if Has_Invariants (Priv_T) then
          Set_Has_Invariants (Full_T);
-         Set_Has_Invariants (Priv_T);
+         Set_Invariant_Procedure (Full_T, Invariant_Procedure (Priv_T));
       end if;
 
-      if Has_Inheritable_Invariants (Full_T)
-           or else
-         Has_Inheritable_Invariants (Priv_T)
-      then
+      if Has_Inheritable_Invariants (Priv_T) then
          Set_Has_Inheritable_Invariants (Full_T);
-         Set_Has_Inheritable_Invariants (Priv_T);
-      end if;
-
-      --  This is where we build the invariant procedure if needed
-
-      if Has_Invariants (Priv_T) then
-         declare
-            PDecl : Entity_Id;
-            PBody : Entity_Id;
-            Packg : constant Node_Id := Declaration_Node (Scope (Priv_T));
-
-         begin
-            Build_Invariant_Procedure (Full_T, PDecl, PBody);
-
-            --  Error defense, normally these should be set
-
-            if Present (PDecl) and then Present (PBody) then
-
-               --  Spec goes at the end of the public part of the package.
-               --  That's behind us, so we have to manually analyze the
-               --  inserted spec.
-
-               Append_To (Visible_Declarations (Packg), PDecl);
-               Analyze (PDecl);
-
-               --  Body goes at the end of the private part of the package.
-               --  That's ahead of us so it will get analyzed later on when
-               --  we come to it.
-
-               Append_To (Private_Declarations (Packg), PBody);
-
-               --  Copy Invariant procedure to private declaration
-
-               Set_Invariant_Procedure (Priv_T, Invariant_Procedure (Full_T));
-               Set_Has_Invariants (Priv_T);
-            end if;
-         end;
       end if;
 
       --  Propagate predicates to full type
@@ -17300,17 +17980,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);
@@ -17368,20 +18048,31 @@ 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;
-      Type_Decl : Node_Id;
-      Def_Id    : Entity_Id;
+      Lo, Hi      : Node_Id;
+      R_Checks    : Check_Result;
+      Insert_Node : Node_Id;
+      Def_Id      : Entity_Id;
 
    begin
       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);
 
@@ -17484,32 +18175,43 @@ package body Sem_Ch3 is
             if not R_Check_Off then
                R_Checks := Get_Range_Checks (R, T);
 
-               --  Look up tree to find an appropriate insertion point.
-               --  This seems really junk code, and very brittle, couldn't
-               --  we just use an insert actions call of some kind ???
-
-               Type_Decl := Parent (R);
-               while Present (Type_Decl) and then not
-                 (Nkind_In (Type_Decl, N_Full_Type_Declaration,
-                                       N_Subtype_Declaration,
-                                       N_Loop_Statement,
-                                       N_Task_Type_Declaration)
-                    or else
-                  Nkind_In (Type_Decl, N_Single_Task_Declaration,
-                                       N_Protected_Type_Declaration,
-                                       N_Single_Protected_Declaration))
-               loop
-                  Type_Decl := Parent (Type_Decl);
+               --  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
+               --  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,
+               --  pragma, or declaration.
+
+               Insert_Node := Parent (R);
+               while Present (Insert_Node) loop
+                  exit when
+                    Nkind (Insert_Node) in N_Declaration
+                    and then
+                      not Nkind_In
+                        (Insert_Node, N_Component_Declaration,
+                                      N_Loop_Parameter_Specification,
+                                      N_Function_Specification,
+                                      N_Procedure_Specification);
+
+                  exit when Nkind (Insert_Node) in N_Later_Decl_Item
+                    or else Nkind (Insert_Node) in
+                              N_Statement_Other_Than_Procedure_Call
+                    or else Nkind_In (Insert_Node, N_Procedure_Call_Statement,
+                                                   N_Pragma);
+
+                  Insert_Node := Parent (Insert_Node);
                end loop;
 
                --  Why would Type_Decl not be present???  Without this test,
                --  short regression tests fail.
 
-               if Present (Type_Decl) then
+               if Present (Insert_Node) then
 
-                  --  Case of loop statement (more comments ???)
+                  --  Case of loop statement. Verify that the range is part
+                  --  of the subtype indication of the iteration scheme.
 
-                  if Nkind (Type_Decl) = N_Loop_Statement then
+                  if Nkind (Insert_Node) = N_Loop_Statement then
                      declare
                         Indic : Node_Id;
 
@@ -17526,18 +18228,20 @@ package body Sem_Ch3 is
 
                            Insert_Range_Checks
                              (R_Checks,
-                              Type_Decl,
+                              Insert_Node,
                               Def_Id,
-                              Sloc (Type_Decl),
+                              Sloc (Insert_Node),
                               R,
                               Do_Before => True);
                         end if;
                      end;
 
-                  --  All other cases (more comments ???)
+                  --  Insertion before a declaration. If the declaration
+                  --  includes discriminants, the list of applicable checks
+                  --  is given by the caller.
 
-                  else
-                     Def_Id := Defining_Identifier (Type_Decl);
+                  elsif Nkind (Insert_Node) in N_Declaration then
+                     Def_Id := Defining_Identifier (Insert_Node);
 
                      if (Ekind (Def_Id) = E_Record_Type
                           and then Depends_On_Discriminant (R))
@@ -17546,18 +18250,29 @@ package body Sem_Ch3 is
                           and then Has_Discriminants (Def_Id))
                      then
                         Append_Range_Checks
-                          (R_Checks, Check_List, Def_Id, Sloc (Type_Decl), R);
+                          (R_Checks,
+                            Check_List, Def_Id, Sloc (Insert_Node), R);
 
                      else
                         Insert_Range_Checks
-                          (R_Checks, Type_Decl, Def_Id, Sloc (Type_Decl), R);
+                          (R_Checks,
+                            Insert_Node, Def_Id, Sloc (Insert_Node), R);
 
                      end if;
+
+                  --  Insertion before a statement. Range appears in the
+                  --  context of a quantified expression. Insertion will
+                  --  take place when expression is expanded.
+
+                  else
+                     null;
                   end if;
                end if;
             end if;
          end if;
 
+      --  Case of other than an explicit N_Range node
+
       elsif Expander_Active then
          Get_Index_Bounds (R, Lo, Hi);
          Force_Evaluation (Lo);
@@ -18235,7 +18950,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 =>
@@ -18274,10 +18989,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;
 
@@ -18368,6 +19088,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
@@ -18387,6 +19115,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);
 
@@ -18525,6 +19255,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
@@ -18547,12 +19311,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;
@@ -18921,6 +19688,81 @@ package body Sem_Ch3 is
       Set_Ekind          (T, E_Signed_Integer_Subtype);
       Set_Etype          (T, Implicit_Base);
 
+      --  In formal verification mode, override partially the decisions above
+      --  to restrict 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 ALFA_Mode then
+
+         --  If the range of the type is already symmetric with a possible
+         --  extra negative value, just make the type its own base type.
+
+         if UI_Le (Lo_Val, Hi_Val)
+           and then (UI_Eq (Lo_Val, UI_Negate (Hi_Val))
+                      or else
+                        UI_Eq (Lo_Val, UI_Sub (UI_Negate (Hi_Val), Uint_1)))
+         then
+            Set_Etype (T, T);
+
+         else
+            declare
+               Sym_Hi_Val : Uint;
+               Sym_Lo_Val : Uint;
+               Decl       : Node_Id;
+               Dloc       : constant Source_Ptr := Sloc (Def);
+               Lbound     : Node_Id;
+               Ubound     : 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);
+
+               Decl := Make_Full_Type_Declaration (Dloc,
+                 Defining_Identifier => Implicit_Base,
+                 Type_Definition     =>
+                   Make_Signed_Integer_Type_Definition (Dloc,
+                     Low_Bound  => Lbound,
+                     High_Bound => Ubound));
+
+               Analyze (Decl);
+               Set_Etype (Implicit_Base, Implicit_Base);
+               Insert_Before (Parent (Def), Decl);
+            end;
+         end if;
+      end if;
+
       Set_Size_Info      (T,                (Implicit_Base));
       Set_First_Rep_Item (T, First_Rep_Item (Implicit_Base));
       Set_Scalar_Range   (T, Def);