[multiple changes]

2011-09-02  Bob Duff  <duff@adacore.com>

	* sem_ch6.adb: (Check_Post_State): Suppress warning
	"postcondition refers only to pre-state" when the expression has not
	yet been analyzed, because it causes false alarms. This can happen when
	the postcondition contains a quantified expression, because those are
	analyzed later. This is a temporary/partial fix.
	(Process_Post_Conditions): Minor: change wording of warning.

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

	* sem_ch3.adb (Analyze_Object_Declaration): Detect the violation of
	illegal use of unconstrained string type in SPARK mode.
	* sem_res.adb (Analyze_Operator_Symbol): Set the
	right place where the string operand of concatenation should be
	violate in SPARK mode.

From-SVN: r178460

4 files changed, 39 insertions, 6 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 91b2ebf..4ca7037 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,20 @@
+2011-09-02  Bob Duff  <duff@adacore.com>
+
+	* sem_ch6.adb: (Check_Post_State): Suppress warning
+	"postcondition refers only to pre-state" when the expression has not
+	yet been analyzed, because it causes false alarms. This can happen when
+	the postcondition contains a quantified expression, because those are
+	analyzed later. This is a temporary/partial fix.
+	(Process_Post_Conditions): Minor: change wording of warning.
+
+2011-09-02  Marc Sango  <sango@adacore.com>
+
+	* sem_ch3.adb (Analyze_Object_Declaration): Detect the violation of
+	illegal use of unconstrained string type in SPARK mode.
+	* sem_res.adb (Analyze_Operator_Symbol): Set the
+	right place where the string operand of concatenation should be
+	violate in SPARK mode.
+
 2011-09-02  Robert Dewar  <dewar@adacore.com>
 
 	* sem_prag.adb, sem_util.adb, sem_ch6.adb, prj-nmsc.adb,
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 4102bea..fb702f3 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -3313,9 +3313,18 @@ package body Sem_Ch3 is
          --  Case of initialization present
 
          else
+
             --  Not allowed in Ada 83
 
             if not Constant_Present (N) then
+
+               --  A declaration of unconstrained type in SPARK is limited,
+               --  the only exception to this is the admission of declaration
+               --  of constants of type string.
+
+               Check_SPARK_Restriction
+                 ("declaration of unconstrained type is limited", E);
+
                if Ada_Version = Ada_83
                  and then Comes_From_Source (Object_Definition (N))
                then
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 32c2dbb..bd1b6e3 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -5551,9 +5551,16 @@ package body Sem_Ch6 is
                declare
                   E : constant Entity_Id := Entity (N);
                begin
-                  if Is_Entity_Name (N)
-                    and then Present (E)
-                    and then Ekind (E) in Assignable_Kind
+                  --  ???Quantified expressions get analyzed later, so E can be
+                  --  empty at this point. In this case, we suppress the
+                  --  warning, just in case E is assignable. It seems better to
+                  --  have false negatives than false positives. At some point,
+                  --  we should make the warning more accurate, either by
+                  --  analyzing quantified expressions earlier, or moving this
+                  --  processing later.
+
+                  if No (E) or else
+                    (Is_Entity_Name (N) and then Ekind (E) in Assignable_Kind)
                   then
                      Found := True;
                   end if;
@@ -5627,7 +5634,7 @@ package body Sem_Ch6 is
                Ignored := Find_Post_State (Arg);
 
                if not Post_State_Mentioned then
-                  Error_Msg_N ("?postcondition only refers to pre-state",
+                  Error_Msg_N ("?postcondition refers only to pre-state",
                                Prag);
                end if;
             end if;
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 7668aa9..0a15075 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -7741,7 +7741,7 @@ package body Sem_Res is
       if Is_Character_Type (Etype (Arg)) then
          if not Is_Static_Expression (Arg) then
             Check_SPARK_Restriction
-              ("character operand for concatenation should be static", N);
+              ("character operand for concatenation should be static", Arg);
          end if;
 
       elsif Is_String_Type (Etype (Arg)) then
@@ -7750,7 +7750,7 @@ package body Sem_Res is
            and then not Is_Static_Expression (Arg)
          then
             Check_SPARK_Restriction
-              ("string operand for concatenation should be static", N);
+              ("string operand for concatenation should be static", Arg);
          end if;
 
       --  Do not issue error on an operand that is neither a character nor a