[multiple changes]

2017-04-27  Ed Schonberg  <schonberg@adacore.com>

	* freeze.adb (Build_Inherited_Condition_Pragmas): New procedure,
	subsidiary of Check_Inherited_Conditions, to build pragmas for an
	operation whose ancestor has classwide pre/postconditions. This
	is used both to check the legality of the inheritance in Ada
	and in SPARK, and to determine whether a wrapper is needed for
	an inherited operation.
	* exp_util.adb (Build_Class_Wide_Expression, Replace_Entity):
	Improve placement of error message for inherited classwide
	conditions that become illegal on type derivation.

2017-04-27  Yannick Moy  <moy@adacore.com>

	* sem_ch12.adb (Analyze_Generic_Package_Declaration): Set
	SPARK_Mode from context on generic package.
	* sem_ch7.adb (Analyze_Package_Declaration): Simplify code to remove
	useless test.

2017-04-27  Claire Dross  <dross@adacore.com>

	* a-cofuve.ads (Range_Shifted): Rewrite precondition to avoid
	overflows in computations.
	* a-cofove.ads (Capacity_Range): Rewrite last bound to avoid
	overflows in computations.
	(Insert): Rewrite precondition to avoid overflows in computations.
	* a-cfinve.ads (Capacity_Range): Rewrite last bound to avoid
	overflows in computations.
	(Insert): Rewrite precondition to avoid overflows in computations.

From-SVN: r247318

gcc/ada/ChangeLog

+2017-04-27  Ed Schonberg  <schonberg@adacore.com>
+
+	* freeze.adb (Build_Inherited_Condition_Pragmas): New procedure,
+	subsidiary of Check_Inherited_Conditions, to build pragmas for an
+	operation whose ancestor has classwide pre/postconditions. This
+	is used both to check the legality of the inheritance in Ada
+	and in SPARK, and to determine whether a wrapper is needed for
+	an inherited operation.
+	* exp_util.adb (Build_Class_Wide_Expression, Replace_Entity):
+	Improve placement of error message for inherited classwide
+	conditions that become illegal on type derivation.
+
+2017-04-27  Yannick Moy  <moy@adacore.com>
+
+	* sem_ch12.adb (Analyze_Generic_Package_Declaration): Set
+	SPARK_Mode from context on generic package.
+	* sem_ch7.adb (Analyze_Package_Declaration): Simplify code to remove
+	useless test.
+
+2017-04-27  Claire Dross  <dross@adacore.com>
+
+	* a-cofuve.ads (Range_Shifted): Rewrite precondition to avoid
+	overflows in computations.
+	* a-cofove.ads (Capacity_Range): Rewrite last bound to avoid
+	overflows in computations.
+	(Insert): Rewrite precondition to avoid overflows in computations.
+	* a-cfinve.ads (Capacity_Range): Rewrite last bound to avoid
+	overflows in computations.
+	(Insert): Rewrite precondition to avoid overflows in computations.
+
 2017-04-27  Steve Baird  <baird@adacore.com>
 
 	* exp_ch9.adb (Expand_N_Asynchronous_Select): Initialize the Cancel

gcc/ada/a-cfinve.ads

@@ -63,8 +63,18 @@ is
 
    No_Index : constant Extended_Index := Extended_Index'First;
 
-   subtype Capacity_Range is
-     Count_Type range 0 .. Count_Type (Index_Type'Last - Index_Type'First + 1);
+   Last_Count : constant Count_Type :=
+     (if Index_Type'Last < Index_Type'First then 0
+      elsif Index_Type'Last < -1
+        or else Index_Type'Pos (Index_Type'First) >
+          Index_Type'Pos (Index_Type'Last) - Count_Type'Last
+      then Index_Type'Pos (Index_Type'Last) -
+          Index_Type'Pos (Index_Type'First) + 1
+      else Count_Type'Last);
+   --  Maximal capacity of any vector. It is the minimum of the size of the
+   --  index range and the last possible Count_Type.
+
+   subtype Capacity_Range is Count_Type range 0 .. Last_Count;
 
    type Vector (Capacity : Capacity_Range) is limited private with
      Default_Initial_Condition => Is_Empty (Vector);
@@ -295,7 +305,8 @@ is
      Pre    =>
        Length (Container) <= Capacity (Container) - Length (New_Item)
          and (Before in Index_Type'First .. Last_Index (Container)
-              or Before - 1 = Last_Index (Container)),
+              or (Before /= No_Index
+                    and then Before - 1 = Last_Index (Container))),
      Post   =>
        Length (Container) = Length (Container)'Old + Length (New_Item)
 
@@ -369,7 +380,8 @@ is
      Pre    =>
        Length (Container) <= Capacity (Container) - Count
          and (Before in Index_Type'First .. Last_Index (Container)
-              or Before - 1 = Last_Index (Container)),
+              or (Before /= No_Index
+                    and then Before - 1 = Last_Index (Container))),
      Post   =>
        Length (Container) = Length (Container)'Old + Count
 

gcc/ada/a-cofove.ads

@@ -57,8 +57,18 @@ is
 
    No_Index : constant Extended_Index := Extended_Index'First;
 
-   subtype Capacity_Range is
-     Count_Type range 0 .. Count_Type (Index_Type'Last - Index_Type'First + 1);
+   Last_Count : constant Count_Type :=
+     (if Index_Type'Last < Index_Type'First then 0
+      elsif Index_Type'Last < -1
+        or else Index_Type'Pos (Index_Type'First) >
+          Index_Type'Pos (Index_Type'Last) - Count_Type'Last
+      then Index_Type'Pos (Index_Type'Last) -
+          Index_Type'Pos (Index_Type'First) + 1
+      else Count_Type'Last);
+   --  Maximal capacity of any vector. It is the minimum of the size of the
+   --  index range and the last possible Count_Type.
+
+   subtype Capacity_Range is Count_Type range 0 .. Last_Count;
 
    type Vector (Capacity : Capacity_Range) is limited private with
      Default_Initial_Condition => Is_Empty (Vector);
@@ -289,7 +299,8 @@ is
      Pre    =>
        Length (Container) <= Capacity (Container) - Length (New_Item)
          and (Before in Index_Type'First .. Last_Index (Container)
-              or Before - 1 = Last_Index (Container)),
+              or (Before /= No_Index
+                    and then Before - 1 = Last_Index (Container))),
      Post   =>
        Length (Container) = Length (Container)'Old + Length (New_Item)
 
@@ -363,7 +374,8 @@ is
      Pre    =>
        Length (Container) <= Capacity (Container) - Count
          and (Before in Index_Type'First .. Last_Index (Container)
-              or Before - 1 = Last_Index (Container)),
+              or (Before /= No_Index
+                    and then Before - 1 = Last_Index (Container))),
      Post   =>
        Length (Container) = Length (Container)'Old + Count
 

gcc/ada/a-cofuve.ads

@@ -225,10 +225,16 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is
      Global => null,
      Pre    =>
        Lst <= Last (Left)
-         and Offset in
-           Index_Type'Pos (Index_Type'First) - Index_Type'Pos (Fst) ..
-             (Index_Type'Pos (Index_Type'First) - 1) + Length (Right) -
-              Index_Type'Pos (Lst),
+         and then
+           (if Offset < 0 then
+              Index_Type'Pos (Index_Type'Base'First) - Offset <=
+              Index_Type'Pos (Index_Type'First))
+         and then
+           (if Fst <= Lst then
+              Offset in
+                Index_Type'Pos (Index_Type'First) - Index_Type'Pos (Fst) ..
+                  (Index_Type'Pos (Index_Type'First) - 1) + Length (Right) -
+                   Index_Type'Pos (Lst)),
      Post   =>
        Range_Shifted'Result =
          ((for all I in Fst .. Lst =>

gcc/ada/exp_util.adb

@@ -1135,9 +1135,17 @@ package body Exp_Util is
                  and then Is_Abstract_Subprogram (Entity (N))
                then
                   Error_Msg_Sloc := Sloc (Current_Scope);
-                  Error_Msg_NE
-                    ("cannot call abstract subprogram in inherited condition "
-                      & "for&#", N, Current_Scope);
+                  --  Error_Msg_Node_1 := Entity (N);
+                  Error_Msg_Node_2 := Subp;
+                  if Comes_From_Source (Subp) then
+                     Error_Msg_NE
+                       ("cannot call abstract subprogram& in inherited "
+                         & "condition for&#", Subp, Entity (N));
+                  else
+                     Error_Msg_NE
+                       ("cannot call abstract subprogram& in inherited "
+                         & "condition for inherited&#", Subp, Entity (N));
+                  end if;
 
                --  In SPARK mode, reject an inherited condition for an
                --  inherited operation if it contains a call to an overriding

gcc/ada/freeze.adb

@@ -1400,20 +1400,72 @@ package body Freeze is
 
    procedure Check_Inherited_Conditions (R : Entity_Id) is
       Prim_Ops      : constant Elist_Id := Primitive_Operations (R);
-      A_Post        : Node_Id;
-      A_Pre         : Node_Id;
       Decls         : List_Id;
       Needs_Wrapper : Boolean;
-      New_Prag      : Node_Id;
       Op_Node       : Elmt_Id;
       Par_Prim      : Entity_Id;
       Prim          : Entity_Id;
 
+      ---------------------------------------
+      -- Build_Inherited_Condition_Pragmas --
+      ---------------------------------------
+
+      procedure Build_Inherited_Condition_Pragmas (Subp : Entity_Id);
+      --  Build corresponding pragmas for an operation whose ancestor has
+      --  class-wide pre/postconditions. If the operation is inherited, the
+      --  pragmas force the creation of a wrapper for the inherited operation.
+      --  If the ancestor is being overridden, the pragmas are constructed only
+      --  to verify their legality, in case they contain calls to other
+      --  primitives that may haven been overridden.
+
+      procedure Build_Inherited_Condition_Pragmas (Subp : Entity_Id) is
+         A_Post   : Node_Id;
+         A_Pre    : Node_Id;
+         New_Prag : Node_Id;
+
+      begin
+         A_Pre := Get_Pragma (Par_Prim, Pragma_Precondition);
+         if Present (A_Pre) and then Class_Present (A_Pre) then
+            New_Prag := New_Copy_Tree (A_Pre);
+            Build_Class_Wide_Expression
+              (Prag          => New_Prag,
+               Subp          => Prim,
+               Par_Subp      => Par_Prim,
+               Adjust_Sloc   => False,
+               Needs_Wrapper => Needs_Wrapper);
+
+            if Needs_Wrapper
+              and then not Comes_From_Source (Subp)
+              and then Expander_Active
+            then
+               Append (New_Prag, Decls);
+            end if;
+         end if;
+
+         A_Post := Get_Pragma (Par_Prim, Pragma_Postcondition);
+
+         if Present (A_Post) and then Class_Present (A_Post) then
+            New_Prag := New_Copy_Tree (A_Post);
+            Build_Class_Wide_Expression
+              (Prag           => New_Prag,
+               Subp           => Prim,
+               Par_Subp       => Par_Prim,
+               Adjust_Sloc    => False,
+               Needs_Wrapper  => Needs_Wrapper);
+
+            if Needs_Wrapper
+              and then not Comes_From_Source (Subp)
+              and then Expander_Active
+            then
+               Append (New_Prag, Decls);
+            end if;
+         end if;
+      end Build_Inherited_Condition_Pragmas;
+
    begin
       Op_Node := First_Elmt (Prim_Ops);
       while Present (Op_Node) loop
-         Prim          := Node (Op_Node);
-         Needs_Wrapper := False;
+         Prim := Node (Op_Node);
 
          --  Map the overridden primitive to the overriding one. This takes
          --  care of all overridings and is done only once.
@@ -1421,7 +1473,29 @@ package body Freeze is
          if Present (Overridden_Operation (Prim))
            and then Comes_From_Source (Prim)
          then
-            Update_Primitives_Mapping (Overridden_Operation (Prim), Prim);
+            Par_Prim := Overridden_Operation (Prim);
+            Update_Primitives_Mapping (Par_Prim, Prim);
+         end if;
+
+         Next_Elmt (Op_Node);
+      end loop;
+
+      --  Now perform validity checks on the inherited conditions of
+      --  overriding operations, for conformance with LSP, and apply
+      --  SPARK-specific restrictions on inherited conditions.
+
+      Op_Node := First_Elmt (Prim_Ops);
+      while Present (Op_Node) loop
+         Prim := Node (Op_Node);
+         if Present (Overridden_Operation (Prim))
+           and then Comes_From_Source (Prim)
+         then
+            Par_Prim := Overridden_Operation (Prim);
+
+            --  Analyze the contract items of the overridden operation, before
+            --  they are rewritten as pragmas.
+
+            Analyze_Entry_Or_Subprogram_Contract (Par_Prim);
 
             --  In SPARK mode this is where we can collect the inherited
             --  conditions, because we do not create the Check pragmas that
@@ -1429,28 +1503,27 @@ package body Freeze is
             --  overriding operations.
 
             if SPARK_Mode = On then
+               Collect_Inherited_Class_Wide_Conditions (Prim);
 
-               --  Analyze the contract items of the parent operation, before
-               --  they are rewritten when inherited.
-
-               Analyze_Entry_Or_Subprogram_Contract
-                 (Overridden_Operation (Prim));
+            else
 
-               --  Now verify the legality of inherited contracts for LSP
-               --  conformance.
+               --  Build the corresponding pragmas to check for legality
+               --  of the inherited condition.
 
-               Collect_Inherited_Class_Wide_Conditions (Prim);
+               Build_Inherited_Condition_Pragmas (Prim);
             end if;
          end if;
 
          Next_Elmt (Op_Node);
       end loop;
 
-      --  In all cases, we examine inherited operations to check whether they
-      --  require a wrapper to handle inherited conditions that call other
-      --  primitives, so that LSP can be verified/enforced.
+      --  Now examine the inherited operations to check whether they require
+      --  a wrapper to handle inherited conditions that call other primitives,
+      --  so that LSP can be verified/enforced.
 
       Op_Node := First_Elmt (Prim_Ops);
+      Needs_Wrapper := False;
+
       while Present (Op_Node) loop
          Decls := Empty_List;
          Prim  := Node (Op_Node);
@@ -1458,45 +1531,19 @@ package body Freeze is
          if not Comes_From_Source (Prim) and then Present (Alias (Prim)) then
             Par_Prim := Alias (Prim);
 
-            --  Analyze the contract items of the parent operation, before
-            --  they are rewritten when inherited.
+            --  Analyze the contract items of the parent operation, and
+            --  determine whether a wrapper is needed. This is determined
+            --  when the condition is rewritten in sem_prag, using the
+            --  mapping between overridden and overriding operations built
+            --  in the loop above.
 
             Analyze_Entry_Or_Subprogram_Contract (Par_Prim);
-
-            A_Pre := Get_Pragma (Par_Prim, Pragma_Precondition);
-
-            if Present (A_Pre) and then Class_Present (A_Pre) then
-               New_Prag := New_Copy_Tree (A_Pre);
-               Build_Class_Wide_Expression
-                 (Prag          => New_Prag,
-                  Subp          => Prim,
-                  Par_Subp      => Par_Prim,
-                  Adjust_Sloc   => False,
-                  Needs_Wrapper => Needs_Wrapper);
-
-               if Needs_Wrapper then
-                  Append (New_Prag, Decls);
-               end if;
-            end if;
-
-            A_Post := Get_Pragma (Par_Prim, Pragma_Postcondition);
-
-            if Present (A_Post) and then Class_Present (A_Post) then
-               New_Prag := New_Copy_Tree (A_Post);
-               Build_Class_Wide_Expression
-                 (Prag           => New_Prag,
-                  Subp           => Prim,
-                  Par_Subp       => Par_Prim,
-                  Adjust_Sloc    => False,
-                  Needs_Wrapper  => Needs_Wrapper);
-
-               if Needs_Wrapper then
-                  Append (New_Prag, Decls);
-               end if;
-            end if;
+            Build_Inherited_Condition_Pragmas (Prim);
          end if;
 
-         if Needs_Wrapper and then not Is_Abstract_Subprogram (Par_Prim) then
+         if Needs_Wrapper and then not Is_Abstract_Subprogram (Par_Prim)
+           and then Expander_Active
+         then
 
             --  We need to build a new primitive that overrides the inherited
             --  one, and whose inherited expression has been updated above.

gcc/ada/sem_ch12.adb

@@ -3382,6 +3382,13 @@ package body Sem_Ch12 is
       Set_Ekind  (Id, E_Generic_Package);
       Set_Etype  (Id, Standard_Void_Type);
 
+      --  Set SPARK_Mode from context
+
+      Set_SPARK_Pragma               (Id, SPARK_Mode_Pragma);
+      Set_SPARK_Aux_Pragma           (Id, SPARK_Mode_Pragma);
+      Set_SPARK_Pragma_Inherited     (Id);
+      Set_SPARK_Aux_Pragma_Inherited (Id);
+
       --  Analyze aspects now, so that generated pragmas appear in the
       --  declarations before building and analyzing the generic copy.
 

gcc/ada/sem_ch7.adb

@@ -975,22 +975,20 @@ package body Sem_Ch7 is
       Set_Ekind  (Id, E_Package);
       Set_Etype  (Id, Standard_Void_Type);
 
-      --  Set SPARK_Mode from context only for non-generic package
+      --  Set SPARK_Mode from context
 
-      if Ekind (Id) = E_Package then
-         Set_SPARK_Pragma               (Id, SPARK_Mode_Pragma);
-         Set_SPARK_Aux_Pragma           (Id, SPARK_Mode_Pragma);
-         Set_SPARK_Pragma_Inherited     (Id);
-         Set_SPARK_Aux_Pragma_Inherited (Id);
+      Set_SPARK_Pragma               (Id, SPARK_Mode_Pragma);
+      Set_SPARK_Aux_Pragma           (Id, SPARK_Mode_Pragma);
+      Set_SPARK_Pragma_Inherited     (Id);
+      Set_SPARK_Aux_Pragma_Inherited (Id);
 
-         --  Save the state of flag Ignore_SPARK_Mode_Pragmas_In_Instance in
-         --  case the body of this package is instantiated or inlined later and
-         --  out of context. The body uses this attribute to restore the value
-         --  of the global flag.
+      --  Save the state of flag Ignore_SPARK_Mode_Pragmas_In_Instance in case
+      --  the body of this package is instantiated or inlined later and out
+      --  of context. The body uses this attribute to restore the value of
+      --  the global flag.
 
-         if Ignore_SPARK_Mode_Pragmas_In_Instance then
-            Set_Ignore_SPARK_Mode_Pragmas (Id);
-         end if;
+      if Ignore_SPARK_Mode_Pragmas_In_Instance then
+         Set_Ignore_SPARK_Mode_Pragmas (Id);
       end if;
 
       --  Analyze aspect specifications immediately, since we need to recognize