[multiple changes]

2011-09-05  Marc Sango  <sango@adacore.com>

	* sem_ch3.adb (Analyze_Object_Declaration): Remove
	the wrong test and add the correct test to detect the violation
	of illegal use of unconstrained string type in SPARK mode.

2011-09-05  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch5.adb (Analyze_Iteration_Specification): Improve error
	message on an iterator over an array.

2011-09-05  Robert Dewar  <dewar@adacore.com>

	* lib-xref-alfa.adb: Minor reformatting.

From-SVN: r178538

gcc/ada/ChangeLog

@@ -1,3 +1,18 @@
+2011-09-05  Marc Sango  <sango@adacore.com>
+
+	* sem_ch3.adb (Analyze_Object_Declaration): Remove
+	the wrong test and add the correct test to detect the violation
+	of illegal use of unconstrained string type in SPARK mode.
+
+2011-09-05  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch5.adb (Analyze_Iteration_Specification): Improve error
+	message on an iterator over an array.
+
+2011-09-05  Robert Dewar  <dewar@adacore.com>
+
+	* lib-xref-alfa.adb: Minor reformatting.
+
 2011-09-05  Robert Dewar  <dewar@adacore.com>
 
 	* sem_ch3.adb, sem_res.adb, par.adb, par-ch6.adb, g-comlin.adb,

gcc/ada/lib-xref-alfa.adb

@@ -586,10 +586,12 @@ package body Alfa is
          function Is_Alfa_Reference
            (E   : Entity_Id;
             Typ : Character) return Boolean;
-         --  Return whether the reference is adequate for this entity
+         --  Return whether entity reference E meets Alfa requirements. Typ
+         --  is the reference type.
 
          function Is_Alfa_Scope (E : Entity_Id) return Boolean;
-         --  Return whether the entity or reference scope is adequate
+         --  Return whether the entity or reference scope meets requirements
+         --  for being an Alfa scope.
 
          function Is_Global_Constant (E : Entity_Id) return Boolean;
          --  Return True if E is a global constant for which we should ignore
@@ -604,35 +606,33 @@ package body Alfa is
             Typ : Character) return Boolean
          is
          begin
+            --  The only references of interest on callable entities are calls.
+            --  On non-callable entities, the only references of interest are
+            --  reads and writes.
 
             if Ekind (E) in Overloadable_Kind then
-
-               --  The only references of interest on callable entities are
-               --  calls.  On non-callable entities, the only references of
-               --  interest are reads and writes.
-
                return Typ = 's';
 
+            --  References to constant objects are not considered in Alfa
+            --  section, as these will be translated as constants in the
+            --  intermediate language for formal verification, and should
+            --  therefore never appear in frame conditions.
+
             elsif Is_Constant_Object (E) then
-
-               --  References to constant objects are not considered in Alfa
-               --  section, as these will be translated as constants in the
-               --  intermediate language for formal verification, and should
-               --  therefore never appear in frame conditions.
-
                   return False;
 
-            elsif Present (Etype (E)) and then
-               Ekind (Etype (E)) in Concurrent_Kind then
-
-               --  Objects of Task type or protected type are not Alfa
-               --  references.
+            --  Objects of Task type or protected type are not Alfa references
 
+            elsif Present (Etype (E))
+              and then Ekind (Etype (E)) in Concurrent_Kind
+            then
                return False;
 
+            --  In all other cases, result is true for reference/modify cases,
+            --  and false for all other cases.
+
             else
                return Typ = 'r' or else Typ = 'm';
-
             end if;
          end Is_Alfa_Reference;
 

gcc/ada/sem_ch3.adb

@@ -3267,6 +3267,16 @@ package body Sem_Ch3 is
 
       if Is_Indefinite_Subtype (T) then
 
+         --  In SPARK, a declaration of unconstrained type is allowed
+         --  only for constants of type string.
+
+         if Is_String_Type (T)
+           and then not Constant_Present (Original_Node (N)) then
+            Check_SPARK_Restriction
+              ("declaration of object of unconstrained type not allowed",
+               N);
+         end if;
+
          --  Nothing to do in deferred constant case
 
          if Constant_Present (N) and then No (E) then
@@ -3313,21 +3323,10 @@ package body Sem_Ch3 is
          --  Case of initialization present
 
          else
-            --  Check restrictions in Ada 83 and SPARK modes
+            --  Check restrictions in Ada 83
 
             if not Constant_Present (N) then
 
-               --  In SPARK, a declaration of unconstrained type is allowed
-               --  only for constants of type string.
-
-               --  Isn't following check the wrong way round???
-
-               if Nkind (E) = N_String_Literal then
-                  Check_SPARK_Restriction
-                    ("declaration of object of unconstrained type not allowed",
-                     E);
-               end if;
-
                --  Unconstrained variables not allowed in Ada 83 mode
 
                if Ada_Version = Ada_83

gcc/ada/sem_ch5.adb

@@ -2336,13 +2336,18 @@ package body Sem_Ch5 is
       if Is_Array_Type (Typ) then
          if Of_Present (N) then
             Set_Etype (Def_Id, Component_Type (Typ));
+
+         elsif Ada_Version < Ada_2012 then
+            Error_Msg_N
+              ("missing Range attribute in iteration over an array", N);
+
          else
             Error_Msg_N
               ("to iterate over the elements of an array, use OF", N);
 
             --  Prevent cascaded errors
 
-            Set_Ekind (Def_Id, E_Constant);
+            Set_Ekind (Def_Id, E_Loop_Parameter);
             Set_Etype (Def_Id, Etype (First_Index (Typ)));
          end if;