[multiple changes]

2017-04-27  Ed Schonberg  <schonberg@adacore.com>

	* sem_attr.adb (Analyze_Attribute, case 'Image): In Ada2012 the
	prefix can be an object reference in which case Obj'Image (X)
	can only be interpreted as an indexing of the parameterless
	version of the attribute.
	* par-ch4.adb (P_Name): An attribute reference can be the prefix of
	an indexing or a slice operation if the attribute does not require
	parameters. In Ada2012 'Image also belongs in this category,
	and A'Image (lo .. hi) is legal and must be parsed as a slice.

2017-04-27  Yannick Moy  <moy@adacore.com>

	* exp_ch4.adb: Minor reformatting.
	* gnat1drv.adb (Adjust_Global_Switches): When in GNATprove mode,
	disable the CodePeer and C generation modes. Similar to the
	opposite actions done in CodePeer mode.

From-SVN: r247331

gcc/ada/ChangeLog

+2017-04-27  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_attr.adb (Analyze_Attribute, case 'Image): In Ada2012 the
+	prefix can be an object reference in which case Obj'Image (X)
+	can only be interpreted as an indexing of the parameterless
+	version of the attribute.
+	* par-ch4.adb (P_Name): An attribute reference can be the prefix of
+	an indexing or a slice operation if the attribute does not require
+	parameters. In Ada2012 'Image also belongs in this category,
+	and A'Image (lo .. hi) is legal and must be parsed as a slice.
+
+2017-04-27  Yannick Moy  <moy@adacore.com>
+
+	* exp_ch4.adb: Minor reformatting.
+	* gnat1drv.adb (Adjust_Global_Switches): When in GNATprove mode,
+	disable the CodePeer and C generation modes. Similar to the
+	opposite actions done in CodePeer mode.
+
 2017-04-27  Yannick Moy  <moy@adacore.com>
 
 	* sem_res.adb: Remove duplicate code.

gcc/ada/exp_ch4.adb

@@ -13060,7 +13060,7 @@ package body Exp_Ch4 is
          Result :=
            Make_Op_Le (Loc,
              Left_Opnd  => Left,
-                       Right_Opnd => Right);
+             Right_Opnd => Right);
 
       --  X'Length > 1  => X'First < X'Last
       --  X'Length > n  => X'First + (n = 1) < X'Last

gcc/ada/gnat1drv.adb

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2016, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2017, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -381,6 +381,22 @@ procedure Gnat1drv is
 
       if GNATprove_Mode then
 
+         --  Turn off CodePeer mode (which can be set via e.g. -gnatC or
+         --  -gnateC), not compatible with GNATprove mode.
+
+         CodePeer_Mode := False;
+         Generate_SCIL := False;
+
+         --  Turn off C tree generation, not compatible with GNATprove mode. We
+         --  do not expect this to happen in normal use, since both modes are
+         --  enabled by special tools, but it is useful to turn off these flags
+         --  this way when we are doing GNATprove tests on existing test suites
+         --  that may have -gnateg set, to avoid the need for special casing.
+
+         Modify_Tree_For_C := False;
+         Generate_C_Code := False;
+         Unnest_Subprogram_Mode := False;
+
          --  Turn off inlining, which would confuse formal verification output
          --  and gain nothing.
 

gcc/ada/par-ch4.adb

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2016, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2017, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -47,12 +47,11 @@ package body Ch4 is
       Attribute_Version      => True,
       Attribute_Type_Key     => True,
       others                 => False);
-   --  This map contains True for parameterless attributes that return a
-   --  string or a type. For those attributes, a left parenthesis after
-   --  the attribute should not be analyzed as the beginning of a parameters
-   --  list because it may denote a slice operation (X'Img (1 .. 2)) or
-   --  a type conversion (X'Class (Y)). The Ada2012 attribute 'Old is in
-   --  this category.
+   --  This map contains True for parameterless attributes that return a string
+   --  or a type. For those attributes, a left parenthesis after the attribute
+   --  should not be analyzed as the beginning of a parameters list because it
+   --  may denote a slice operation (X'Img (1 .. 2)) or a type conversion
+   --  (X'Class (Y)). The Ada 2012 attribute 'Old is in this category.
 
    --  Note: Loop_Entry is in this list because, although it can take an
    --  optional argument (the loop name), we can't distinguish that at parse
@@ -587,8 +586,35 @@ package body Ch4 is
                         --  Here for normal case (not => for named parameter)
 
                         else
-                           Append (Expr, Expressions (Name_Node));
-                           exit when not Comma_Present;
+                           --  Special handling for 'Image in Ada 2012, where
+                           --  the attribute can be parameterless and its value
+                           --  can be the prefix of a slice. Rewrite name as a
+                           --  a slice, Expr is its low bound.
+
+                           if Token = Tok_Dot_Dot
+                             and then Attr_Name = Name_Image
+                             and then Ada_Version >= Ada_2012
+                           then
+                              Set_Expressions (Name_Node, No_List);
+                              Prefix_Node := Name_Node;
+                              Name_Node :=
+                                New_Node (N_Slice, Sloc (Prefix_Node));
+                              Set_Prefix (Name_Node, Prefix_Node);
+                              Range_Node := New_Node (N_Range, Token_Ptr);
+                              Set_Low_Bound (Range_Node, Expr);
+                              Scan; -- past ..
+                              Expr_Node := P_Expression;
+                              Check_Simple_Expression (Expr_Node);
+                              Set_High_Bound (Range_Node, Expr_Node);
+                              Set_Discrete_Range (Name_Node, Range_Node);
+                              T_Right_Paren;
+
+                              goto Scan_Name_Extension;
+
+                           else
+                              Append (Expr, Expressions (Name_Node));
+                              exit when not Comma_Present;
+                           end if;
                         end if;
                      end;
                   end loop;

gcc/ada/sem_attr.adb

@@ -4042,10 +4042,25 @@ package body Sem_Attr is
            and then Is_Object_Reference (P)
            and then Is_Scalar_Type (P_Type)
          then
-            Rewrite (N,
-              Make_Attribute_Reference (Loc,
-                Prefix         => Relocate_Node (P),
-                Attribute_Name => Name_Img));
+            if No (Expressions (N)) then
+               Rewrite (N,
+                 Make_Attribute_Reference (Loc,
+                   Prefix         => Relocate_Node (P),
+                   Attribute_Name => Name_Img));
+
+            --  If the attribute reference includes expressions, the
+            --  only possible interpretation is as an indexing of the
+            --  parameterless version of 'Image, so rewrite it accordingly.
+
+            else
+               Rewrite (N,
+                  Make_Indexed_Component (Loc,
+                     Prefix      =>
+                       Make_Attribute_Reference (Loc,
+                         Prefix         => Relocate_Node (P),
+                         Attribute_Name => Name_Img),
+                     Expressions => Expressions (N)));
+            end if;
             Analyze (N);
             return;