[multiple changes]

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

	* gnat_rm.texi: Minor reformatting.
	* sem_prag.adb: Minor reformatting.

2011-08-02  Tristan Gingold  <gingold@adacore.com>

	* vms_data.ads: Add VMS qualifier for -gnateP.

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

	* par-ch13.adb (P_Aspect_Specification): New meaning of Decl = Empty
	* par-ch7.adb (P_Package): Proper placement of aspects for package
	decl/instantiation.
	* par-endh.adb (Check_End): Ad Is_Sloc parameter
	(End_Statements): Add Is_Sloc parameterr
	* par.adb (P_Aspect_Specification): New meaning of Decl = Empty
	(Check_End): Ad Is_Sloc parameter
	(End_Statements): Add Is_Sloc parameterr

2011-08-02  Vincent Celier  <celier@adacore.com>

	* ug_words: Add VMS qualifier equivalent to -gnateP:
	/SYMBOL_PREPROCESSING.

2011-08-02  Jose Ruiz  <ruiz@adacore.com>

	* gnat-style.texi: For hexadecimal numeric literals the typical
	grouping of digits is 4 to represent 2 bytes.
	A procedure spec which is split into several lines is indented two
	characters.

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

	* exp_aggr.adb (Is_Others_Aggregate): move function to other unit.
	* sem_aggr.adb, sem_aggr.ads (Is_Others_Aggregate): move function here
	(Resolve_Aggregate): issue errors in formal modes when aggregate is not
	properly qualified
	(Resolve_Array_Aggregate): issue errors in formal modes on non-static
	choice in array aggregate
	(Resolve_Extension_Aggregate): issue errors in formal modes on subtype
	mark as ancestor
	(Resolve_Record_Aggregate): issue errors in formal modes on mixed
	positional and named aggregate for record, or others in record
	aggregate, or multiple choice in record aggregate
	* sem_res.adb (Resolve_Logical_Op): issue errors in formal mode when
	array operands to logical operations AND, OR and XOR do not have the
	same static lower and higher bounds
	* sem_ch5.adb, sinfo.ads: Correct typos in comments

From-SVN: r177086

1 files changed, 51 insertions, 0 deletions

diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 6cda48e..319b2ff 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -7156,6 +7156,57 @@ package body Sem_Res is
       Set_Etype (N, B_Typ);
       Generate_Operator_Reference (N, B_Typ);
       Eval_Logical_Op (N);
+
+      --  In SPARK or ALFA, logical operations AND, OR and XOR for arrays are
+      --  defined only when both operands have same static lower and higher
+      --  bounds.
+
+      if Formal_Verification_Mode
+        and then Comes_From_Source (Original_Node (N))
+        and then Is_Array_Type (Etype (N))
+      then
+         declare
+            L_Index : Node_Id;
+            R_Index : Node_Id;
+            L_Low   : Node_Id;
+            L_High  : Node_Id;
+            R_Low   : Node_Id;
+            R_High  : Node_Id;
+
+            L_Typ : constant Node_Id := Etype (Left_Opnd (N));
+            R_Typ : constant Node_Id := Etype (Right_Opnd (N));
+
+         begin
+            L_Index := First_Index (L_Typ);
+            R_Index := First_Index (R_Typ);
+
+            Get_Index_Bounds (L_Index, L_Low, L_High);
+            Get_Index_Bounds (R_Index, R_Low, R_High);
+
+            --  Another error is issued for constrained array types with
+            --  non-static bounds elsewhere, so only deal with different
+            --  constrained types, or unconstrained types.
+
+            if L_Typ /= R_Typ or else not Is_Constrained (L_Typ) then
+               if not Is_Static_Expression (L_Low)
+                 or else not Is_Static_Expression (R_Low)
+                 or else Expr_Value (L_Low) /= Expr_Value (R_Low)
+               then
+                  Error_Msg_F ("|~~operation defined only when both operands "
+                               & "have the same static lower bound", N);
+               end if;
+
+               if not Is_Static_Expression (L_High)
+                 or else not Is_Static_Expression (R_High)
+                 or else Expr_Value (L_High) /= Expr_Value (R_High)
+               then
+                  Error_Msg_F ("|~~operation defined only when both operands "
+                               & "have the same static higher bound", N);
+               end if;
+            end if;
+         end;
+      end if;
+
    end Resolve_Logical_Op;
 
    ---------------------------