[multiple changes]

2016-04-18  Yannick Moy  <moy@adacore.com>

	* sem_util.adb (Apply_Compile_Time_Constraint_Error): Do not generate
	raise node in GNATprove mode.

2016-04-18  Hristian Kirtchev  <kirtchev@adacore.com>

	* s-fileio.adb: Minor reformatting.
	* sem_prag.adb (Analyze_Input_Item): Add local
	variable Input_OK. Do not consider mappings of generic formal
	parameters to actuals.

2016-04-18  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch5.adb (Get_Cursor_Type): If iterator type is a derived
	type, the cursor is declared in the scope of the parent type.
	(Analyze_Parameter_Specification): A qualified expression with an
	iterator type indicates an iteration over a container (explicit
	or implicit).

From-SVN: r235139

gcc/ada/ChangeLog

+2016-04-18  Yannick Moy  <moy@adacore.com>
+
+	* sem_util.adb (Apply_Compile_Time_Constraint_Error): Do not generate
+	raise node in GNATprove mode.
+
+2016-04-18  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* s-fileio.adb: Minor reformatting.
+	* sem_prag.adb (Analyze_Input_Item): Add local
+	variable Input_OK. Do not consider mappings of generic formal
+	parameters to actuals.
+
+2016-04-18  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch5.adb (Get_Cursor_Type): If iterator type is a derived
+	type, the cursor is declared in the scope of the parent type.
+	(Analyze_Parameter_Specification): A qualified expression with an
+	iterator type indicates an iteration over a container (explicit
+	or implicit).
+
 2016-04-18  Arnaud Charlet  <charlet@adacore.com>
 
 	* osint-c.ads, osint-c.adb (Delete_C_File, Delete_H_File): New.

gcc/ada/s-fileio.adb

@@ -1057,8 +1057,12 @@ package body System.File_IO is
 
          else
             Fopen_Mode
-              (Namestr, Mode, Text_Encoding in Text_Content_Encoding,
-               Creat, Amethod, Fopstr);
+              (Namestr => Namestr,
+               Mode    => Mode,
+               Text    => Text_Encoding in Text_Content_Encoding,
+               Creat   => Creat,
+               Amethod => Amethod,
+               Fopstr  => Fopstr);
 
             --  A special case, if we are opening (OPEN case) a file and the
             --  mode returned by Fopen_Mode is not "r" or "r+", then we first
@@ -1230,8 +1234,12 @@ package body System.File_IO is
 
       else
          Fopen_Mode
-           (File.Name.all, Mode, File.Text_Encoding in Text_Content_Encoding,
-            False, File.Access_Method, Fopstr);
+           (Namestr => File.Name.all,
+            Mode    => Mode,
+            Text    => File.Text_Encoding in Text_Content_Encoding,
+            Creat   => False,
+            Amethod => File.Access_Method,
+            Fopstr  => Fopstr);
 
          File.Stream := freopen
            (File.Name.all'Address, Fopstr'Address, File.Stream,

gcc/ada/sem_ch5.adb

@@ -1795,7 +1795,15 @@ package body Sem_Ch5 is
          Ent : Entity_Id;
 
       begin
-         Ent := First_Entity (Scope (Typ));
+         --  If iterator type is derived, the cursor is declared in the scope
+         --  of the parent type.
+
+         if Is_Derived_Type (Typ) then
+            Ent := First_Entity (Scope (Etype (Typ)));
+         else
+            Ent := First_Entity (Scope (Typ));
+         end if;
+
          while Present (Ent) loop
             exit when Chars (Ent) = Name_Cursor;
             Next_Entity (Ent);
@@ -2747,8 +2755,9 @@ package body Sem_Ch5 is
 
          --  a)  a function call,
          --  b)  an identifier that is not a type,
-         --  c)  an attribute reference 'Old (within a postcondition)
-         --  d)  an unchecked conversion
+         --  c)  an attribute reference 'Old (within a postcondition),
+         --  d)  an unchecked conversion or a qualified expression with
+         --      the proper iterator type.
 
          --  then it is an iteration over a container. It was classified as
          --  a loop specification by the parser, and must be rewritten now
@@ -2758,13 +2767,19 @@ package body Sem_Ch5 is
          --  conversion is always an object.
 
          if Nkind (DS_Copy) = N_Function_Call
+
            or else (Is_Entity_Name (DS_Copy)
                      and then not Is_Type (Entity (DS_Copy)))
+
            or else (Nkind (DS_Copy) = N_Attribute_Reference
                      and then Nam_In (Attribute_Name (DS_Copy),
-                                      Name_Old, Name_Loop_Entry))
-           or else Nkind (DS_Copy) = N_Unchecked_Type_Conversion
+                                      Name_Loop_Entry, Name_Old))
+
            or else Has_Aspect (Etype (DS_Copy), Aspect_Iterable)
+
+           or else Nkind (DS_Copy) = N_Unchecked_Type_Conversion
+           or else (Nkind (DS_Copy) = N_Qualified_Expression
+                     and then Is_Iterator (Etype (DS_Copy)))
          then
             --  This is an iterator specification. Rewrite it as such and
             --  analyze it to capture function calls that may require
@@ -3138,11 +3153,13 @@ package body Sem_Ch5 is
                Set_Parent (DS_Copy, Parent (DS));
                Preanalyze_Range (DS_Copy);
 
-               --  Check for a call to Iterate ()
+               --  Check for a call to Iterate () or an expression with
+               --  an iterator type.
 
                return
-                 Nkind (DS_Copy) = N_Function_Call
-                   and then Needs_Finalization (Etype (DS_Copy));
+                 (Nkind (DS_Copy) = N_Function_Call
+                   and then Needs_Finalization (Etype (DS_Copy)))
+                 or else Is_Iterator (Etype (DS_Copy));
             end;
          end if;
       end Is_Container_Iterator;

gcc/ada/sem_prag.adb

@@ -2826,6 +2826,7 @@ package body Sem_Prag is
 
          procedure Analyze_Input_Item (Input : Node_Id) is
             Input_Id : Entity_Id;
+            Input_OK : Boolean := True;
 
          begin
             --  Null input list
@@ -2868,27 +2869,47 @@ package body Sem_Prag is
                                          E_Variable)
                   then
                      --  The input cannot denote states or objects declared
-                     --  within the related package (SPARK RM 7.1.5(4)). The
-                     --  only exceptions to this are generic formal parameters.
+                     --  within the related package (SPARK RM 7.1.5(4)).
 
-                     if not Ekind_In (Input_Id, E_Generic_In_Out_Parameter,
-                                                E_Generic_In_Parameter)
-                       and then Within_Scope (Input_Id, Current_Scope)
-                     then
-                        Error_Msg_Name_1 := Chars (Pack_Id);
-                        SPARK_Msg_NE
-                          ("input item & cannot denote a visible object or "
-                           & "state of package %", Input, Input_Id);
+                     if Within_Scope (Input_Id, Current_Scope) then
+
+                        --  Do not consider generic formal parameters or their
+                        --  respective mappings to generic formals. Even though
+                        --  the formals appear within the scope of the package,
+                        --  it is allowed for an initialization item to depend
+                        --  on an input item.
+
+                        if Ekind_In (Input_Id, E_Generic_In_Out_Parameter,
+                                               E_Generic_In_Parameter)
+                        then
+                           null;
+
+                        elsif Ekind_In (Input_Id, E_Constant, E_Variable)
+                          and then Present (Corresponding_Generic_Association
+                                     (Declaration_Node (Input_Id)))
+                        then
+                           null;
+
+                        else
+                           Input_OK := False;
+                           Error_Msg_Name_1 := Chars (Pack_Id);
+                           SPARK_Msg_NE
+                             ("input item & cannot denote a visible object or "
+                              & "state of package %", Input, Input_Id);
+                        end if;
+                     end if;
 
                      --  Detect a duplicate use of the same input item
                      --  (SPARK RM 7.1.5(5)).
 
-                     elsif Contains (Inputs_Seen, Input_Id) then
+                     if Contains (Inputs_Seen, Input_Id) then
+                        Input_OK := False;
                         SPARK_Msg_N ("duplicate input item", Input);
+                     end if;
 
                      --  Input is legal, add it to the list of processed inputs
 
-                     else
+                     if Input_OK then
                         Append_New_Elmt (Input_Id, Inputs_Seen);
 
                         if Ekind (Input_Id) = E_Abstract_State then

gcc/ada/sem_util.adb

@@ -599,7 +599,13 @@ package body Sem_Util is
       Discard_Node
         (Compile_Time_Constraint_Error (N, Msg, Ent, Loc, Warn => Warn));
 
-      if not Rep then
+      --  In GNATprove mode, do not replace the node with an exception raised.
+      --  In such a case, either the call to Compile_Time_Constraint_Error
+      --  issues an error which stops analysis, or it issues a warning in
+      --  a few cases where a suitable check flag is set for GNATprove to
+      --  generate a check message.
+
+      if not Rep or GNATprove_Mode then
          return;
       end if;