[multiple changes]

2011-08-02  Yannick Moy  <moy@adacore.com>

	* sem_attr.adb (Check_Formal_Restriction_On_Attribute): new procedure
	to issue an error in formal mode on attribute not supported in this mode
	(Analyze_Attribute): issue errors on standard attributes not supported
	in formal mode.
	* sem_ch3.adb (Modular_Type_Declaration): remove obsolete part of
	comment, and issue error in formal mode on modulus which is not a power
	of 2.
	(Process_Range_Expr_In_Decl): issue error in formal mode on non-static
	range.
	* sem_ch8.adb (Find_Type): issue error in formal mode on 'Base in
	subtype mark.
	* sem_res.adb (Resolve_Unary_Op): issue error in formal mode on unary
	operator on modular type (except 'not').

2011-08-02  Robert Dewar  <dewar@adacore.com>

	* gnat_rm.texi: Minor reformatting.

From-SVN: r177118

gcc/ada/ChangeLog

+2011-08-02  Yannick Moy  <moy@adacore.com>
+
+	* sem_attr.adb (Check_Formal_Restriction_On_Attribute): new procedure
+	to issue an error in formal mode on attribute not supported in this mode
+	(Analyze_Attribute): issue errors on standard attributes not supported
+	in formal mode.
+	* sem_ch3.adb (Modular_Type_Declaration): remove obsolete part of
+	comment, and issue error in formal mode on modulus which is not a power
+	of 2.
+	(Process_Range_Expr_In_Decl): issue error in formal mode on non-static
+	range.
+	* sem_ch8.adb (Find_Type): issue error in formal mode on 'Base in
+	subtype mark.
+	* sem_res.adb (Resolve_Unary_Op): issue error in formal mode on unary
+	operator on modular type (except 'not').
+
+2011-08-02  Robert Dewar  <dewar@adacore.com>
+
+	* gnat_rm.texi: Minor reformatting.
+
 2011-08-02  Arnaud Charlet  <charlet@adacore.com>
 
 	* s-osinte-linux.ads: Minor comment update and reformatting.

gcc/ada/gnat_rm.texi

@@ -9071,7 +9071,7 @@ passes the compiler in SPARK mode is rejected by the SPARK Examiner,
 e.g. due to the different visibility rules of the Examiner based on
 SPARK @code{inherit} annotations.
 
-SPARK restriction can be useful in providing an initial filter for
+This restriction can be useful in providing an initial filter for
 code developed using SPARK, or in examining legacy code to see how far
 it is from meeting SPARK restrictions.
 

gcc/ada/sem_attr.adb

@@ -289,6 +289,9 @@ package body Sem_Attr is
       --  Common processing for attributes Definite and Has_Discriminants.
       --  Checks that prefix is generic indefinite formal type.
 
+      procedure Check_Formal_Restriction_On_Attribute;
+      --  Issue an error in formal mode because attribute N is allowed
+
       procedure Check_Integer_Type;
       --  Verify that prefix of attribute N is an integer type
 
@@ -565,14 +568,7 @@ package body Sem_Attr is
       --  Start of processing for Analyze_Access_Attribute
 
       begin
-         --  Access attribute is not allowed in SPARK or ALFA
-
-         if Formal_Verification_Mode and then Comes_From_Source (N) then
-            Error_Attr_P ("|~~% attribute is not allowed");
-         end if;
-
-         --  Proceed with analysis
-
+         Check_Formal_Restriction_On_Attribute;
          Check_E0;
 
          if Nkind (P) = N_Character_Literal then
@@ -1293,6 +1289,16 @@ package body Sem_Attr is
          Check_E2;
       end Check_Floating_Point_Type_2;
 
+      -------------------------------------------
+      -- Check_Formal_Restriction_On_Attribute --
+      -------------------------------------------
+
+      procedure Check_Formal_Restriction_On_Attribute is
+      begin
+         Error_Msg_Name_1 := Aname;
+         Check_Formal_Restriction ("attribute % is not allowed", P);
+      end Check_Formal_Restriction_On_Attribute;
+
       ------------------------
       -- Check_Integer_Type --
       ------------------------
@@ -2454,6 +2460,12 @@ package body Sem_Attr is
               ("?redundant attribute, & is its own base type", N, Typ);
          end if;
 
+         if Nkind (Parent (N)) /= N_Attribute_Reference then
+            Error_Msg_Name_1 := Aname;
+            Check_Formal_Restriction
+              ("attribute% is only allowed as prefix of another attribute", P);
+         end if;
+
          Set_Etype (N, Base_Type (Entity (P)));
          Set_Entity (N, Base_Type (Entity (P)));
          Rewrite (N, New_Reference_To (Entity (N), Loc));
@@ -3256,8 +3268,9 @@ package body Sem_Attr is
 
       when Attribute_Image => Image :
       begin
-         Set_Etype (N, Standard_String);
+         Check_Formal_Restriction_On_Attribute;
          Check_Scalar_Type;
+         Set_Etype (N, Standard_String);
 
          if Is_Real_Type (P_Type) then
             if Ada_Version = Ada_83 and then Comes_From_Source (N) then
@@ -3862,6 +3875,14 @@ package body Sem_Attr is
       when Attribute_Pos =>
          Check_Discrete_Type;
          Check_E1;
+
+         if Is_Boolean_Type (P_Type) then
+            Error_Msg_Name_1 := Aname;
+            Error_Msg_Name_2 := Chars (P_Type);
+            Check_Formal_Restriction
+              ("attribute% is not allowed for type%", P);
+         end if;
+
          Resolve (E1, P_Base_Type);
          Set_Etype (N, Universal_Integer);
 
@@ -3880,6 +3901,14 @@ package body Sem_Attr is
       when Attribute_Pred =>
          Check_Scalar_Type;
          Check_E1;
+
+         if Is_Real_Type (P_Type) or else Is_Boolean_Type (P_Type) then
+            Error_Msg_Name_1 := Aname;
+            Error_Msg_Name_2 := Chars (P_Type);
+            Check_Formal_Restriction
+              ("attribute% is not allowed for type%", P);
+         end if;
+
          Resolve (E1, P_Base_Type);
          Set_Etype (N, P_Base_Type);
 
@@ -4414,6 +4443,14 @@ package body Sem_Attr is
       when Attribute_Succ =>
          Check_Scalar_Type;
          Check_E1;
+
+         if Is_Real_Type (P_Type) or else Is_Boolean_Type (P_Type) then
+            Error_Msg_Name_1 := Aname;
+            Error_Msg_Name_2 := Chars (P_Type);
+            Check_Formal_Restriction
+              ("attribute% is not allowed for type%", P);
+         end if;
+
          Resolve (E1, P_Base_Type);
          Set_Etype (N, P_Base_Type);
 
@@ -4731,6 +4768,14 @@ package body Sem_Attr is
       begin
          Check_E1;
          Check_Discrete_Type;
+
+         if Is_Boolean_Type (P_Type) then
+            Error_Msg_Name_1 := Aname;
+            Error_Msg_Name_2 := Chars (P_Type);
+            Check_Formal_Restriction
+              ("attribute% is not allowed for type%", P);
+         end if;
+
          Resolve (E1, Any_Integer);
          Set_Etype (N, P_Base_Type);
 
@@ -4766,6 +4811,7 @@ package body Sem_Attr is
 
       when Attribute_Value => Value :
       begin
+         Check_Formal_Restriction_On_Attribute;
          Check_E1;
          Check_Scalar_Type;
 
@@ -4828,6 +4874,7 @@ package body Sem_Attr is
 
       when Attribute_Wide_Image => Wide_Image :
       begin
+         Check_Formal_Restriction_On_Attribute;
          Check_Scalar_Type;
          Set_Etype (N, Standard_Wide_String);
          Check_E1;
@@ -4854,6 +4901,7 @@ package body Sem_Attr is
 
       when Attribute_Wide_Value => Wide_Value :
       begin
+         Check_Formal_Restriction_On_Attribute;
          Check_E1;
          Check_Scalar_Type;
 
@@ -4894,6 +4942,7 @@ package body Sem_Attr is
       ----------------
 
       when Attribute_Wide_Width =>
+         Check_Formal_Restriction_On_Attribute;
          Check_E0;
          Check_Scalar_Type;
          Set_Etype (N, Universal_Integer);
@@ -4903,6 +4952,7 @@ package body Sem_Attr is
       -----------
 
       when Attribute_Width =>
+         Check_Formal_Restriction_On_Attribute;
          Check_E0;
          Check_Scalar_Type;
          Set_Etype (N, Universal_Integer);

gcc/ada/sem_ch3.adb

@@ -584,8 +584,8 @@ 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
+   --  (implementation restriction).
 
    procedure New_Concatenation_Op (Typ : Entity_Id);
    --  Create an abbreviated declaration for an operator in order to
@@ -16373,6 +16373,7 @@ package body Sem_Ch3 is
          --  Non-binary case
 
          elsif M_Val < 2 ** Bits then
+            Check_Formal_Restriction ("modulus should be a power of 2", T);
             Set_Non_Binary_Modulus (T);
 
             if Bits > System_Max_Nonbinary_Modulus_Power then
@@ -17768,6 +17769,10 @@ package body Sem_Ch3 is
    begin
       Analyze_And_Resolve (R, Base_Type (T));
 
+      if not Is_Static_Range (R) then
+         Check_Formal_Restriction ("range should be static", R);
+      end if;
+
       if Nkind (R) = N_Range then
          Lo := Low_Bound (R);
          Hi := High_Bound (R);

gcc/ada/sem_ch8.adb

@@ -5827,6 +5827,10 @@ package body Sem_Ch8 is
          --  Base attribute, not allowed in Ada 83
 
          elsif Attribute_Name (N) = Name_Base then
+            Error_Msg_Name_1 := Name_Base;
+            Check_Formal_Restriction
+              ("attribute% is only allowed as prefix of another attribute", N);
+
             if Ada_Version = Ada_83 and then Comes_From_Source (N) then
                Error_Msg_N
                  ("(Ada 83) Base attribute not allowed in subtype mark", N);

gcc/ada/sem_res.adb

@@ -9292,6 +9292,12 @@ package body Sem_Res is
       Hi    : Uint;
 
    begin
+      if Is_Modular_Integer_Type (Typ) and then Nkind (N) /= N_Op_Not then
+         Error_Msg_Name_1 := Chars (Typ);
+         Check_Formal_Restriction
+           ("unary operator not defined for modular type%", N);
+      end if;
+
       --  Deal with intrinsic unary operators
 
       if Comes_From_Source (N)