[multiple changes]

2014-11-20  Ed Schonberg  <schonberg@adacore.com>

	* sem_prag.adb (Analyze_Pragma, case Implemented): In ASIS
	(compile-only) mode, use original type declaration to determine
	whether protected type implements an interface.

2014-11-20  Yannick Moy  <moy@adacore.com>

	* a-cfdlli.adb, a-cfdlli.ads, a-cfinve.adb, a-cfinve.ads,
	* a-cofove.adb, a-cofove.ads: Mark spec as SPARK_Mode, and private
	part/body as SPARK_Mode Off.
	* a-cfhama.adb, a-cfhama.ads, a-cfhase.adb, a-cfhase.ads,
	* a-cforma.adb, a-cforma.ads, a-cforse.adb, a-cforse.ads: Use
	aspect instead of pragma for uniformity.

2014-11-20  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_util.adb (Is_EVF_Expression): Include
	attributes 'Loop_Entry, 'Old and 'Update to the logic.

2014-11-20  Bob Duff  <duff@adacore.com>

	* sem_res.adb (Make_Call_Into_Operator): Don't
	call Left_Opnd in the case of unary operators, because they only
	have Right.

From-SVN: r217838

gcc/ada/ChangeLog

@@ -1,3 +1,29 @@
+2014-11-20  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_prag.adb (Analyze_Pragma, case Implemented): In ASIS
+	(compile-only) mode, use original type declaration to determine
+	whether protected type implements an interface.
+
+2014-11-20  Yannick Moy  <moy@adacore.com>
+
+	* a-cfdlli.adb, a-cfdlli.ads, a-cfinve.adb, a-cfinve.ads,
+	* a-cofove.adb, a-cofove.ads: Mark spec as SPARK_Mode, and private
+	part/body as SPARK_Mode Off.
+	* a-cfhama.adb, a-cfhama.ads, a-cfhase.adb, a-cfhase.ads,
+	* a-cforma.adb, a-cforma.ads, a-cforse.adb, a-cforse.ads: Use
+	aspect instead of pragma for uniformity.
+
+2014-11-20  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_util.adb (Is_EVF_Expression): Include
+	attributes 'Loop_Entry, 'Old and 'Update to the logic.
+
+2014-11-20  Bob Duff  <duff@adacore.com>
+
+	* sem_res.adb (Make_Call_Into_Operator): Don't
+	call Left_Opnd in the case of unary operators, because they only
+	have Right.
+
 2014-11-20  Pascal Obry  <obry@adacore.com>
 
 	* initialize.c (ProcListCS): New extern variable (critical section).

gcc/ada/a-cfdlli.adb

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 2010-2013, Free Software Foundation, Inc.         --
+--          Copyright (C) 2010-2014, 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- --
@@ -27,7 +27,9 @@
 
 with System;  use type System.Address;
 
-package body Ada.Containers.Formal_Doubly_Linked_Lists is
+package body Ada.Containers.Formal_Doubly_Linked_Lists with
+  SPARK_Mode => Off
+is
 
    -----------------------
    -- Local Subprograms --

gcc/ada/a-cfdlli.ads

@@ -61,9 +61,11 @@ generic
    with function "=" (Left, Right : Element_Type)
                       return Boolean is <>;
 
-package Ada.Containers.Formal_Doubly_Linked_Lists is
+package Ada.Containers.Formal_Doubly_Linked_Lists with
+  Pure,
+  SPARK_Mode
+is
    pragma Annotate (GNATprove, External_Axiomatization);
-   pragma Pure;
 
    type List (Capacity : Count_Type) is private with
      Iterable => (First       => First,
@@ -337,6 +339,7 @@ package Ada.Containers.Formal_Doubly_Linked_Lists is
    --  scanned yet.
 
 private
+   pragma SPARK_Mode (Off);
 
    type Node_Type is record
       Prev    : Count_Type'Base := -1;

gcc/ada/a-cfhama.adb

@@ -35,8 +35,9 @@ with Ada.Containers.Prime_Numbers; use Ada.Containers.Prime_Numbers;
 
 with System; use type System.Address;
 
-package body Ada.Containers.Formal_Hashed_Maps is
+package body Ada.Containers.Formal_Hashed_Maps with
-   pragma SPARK_Mode (Off);
+  SPARK_Mode => Off
+is
 
    -----------------------
    -- Local Subprograms --

gcc/ada/a-cfhama.ads

@@ -65,10 +65,11 @@ generic
    with function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
    with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
-package Ada.Containers.Formal_Hashed_Maps is
+package Ada.Containers.Formal_Hashed_Maps with
+  Pure,
+  SPARK_Mode
+is
    pragma Annotate (GNATprove, External_Axiomatization);
-   pragma Pure;
-   pragma SPARK_Mode (On);
 
    type Map (Capacity : Count_Type; Modulus : Hash_Type) is private with
      Iterable => (First       => First,
@@ -272,6 +273,8 @@ package Ada.Containers.Formal_Hashed_Maps is
    --  Overlap returns True if the containers have common keys
 
 private
+   pragma SPARK_Mode (Off);
+
    pragma Inline (Length);
    pragma Inline (Is_Empty);
    pragma Inline (Clear);
@@ -282,7 +285,6 @@ private
    pragma Inline (Has_Element);
    pragma Inline (Equivalent_Keys);
    pragma Inline (Next);
-   pragma SPARK_Mode (Off);
 
    type Node_Type is record
       Key         : Key_Type;

gcc/ada/a-cfhase.adb

@@ -35,8 +35,9 @@ with Ada.Containers.Prime_Numbers; use Ada.Containers.Prime_Numbers;
 
 with System; use type System.Address;
 
-package body Ada.Containers.Formal_Hashed_Sets is
+package body Ada.Containers.Formal_Hashed_Sets with
-   pragma SPARK_Mode (Off);
+  SPARK_Mode => Off
+is
 
    -----------------------
    -- Local Subprograms --

gcc/ada/a-cfhase.ads

@@ -67,10 +67,11 @@ generic
 
    with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
-package Ada.Containers.Formal_Hashed_Sets is
+package Ada.Containers.Formal_Hashed_Sets with
+  Pure,
+  SPARK_Mode
+is
    pragma Annotate (GNATprove, External_Axiomatization);
-   pragma Pure;
-   pragma SPARK_Mode (On);
 
    type Set (Capacity : Count_Type; Modulus : Hash_Type) is private with
      Iterable => (First       => First,
@@ -335,9 +336,10 @@ package Ada.Containers.Formal_Hashed_Sets is
    --  scanned yet.
 
 private
-   pragma Inline (Next);
    pragma SPARK_Mode (Off);
 
+   pragma Inline (Next);
+
    type Node_Type is
       record
          Element     : Element_Type;

gcc/ada/a-cfinve.adb

@@ -26,7 +26,9 @@
 -- <http://www.gnu.org/licenses/>.                                          --
 ------------------------------------------------------------------------------
 
-package body Ada.Containers.Formal_Indefinite_Vectors is
+package body Ada.Containers.Formal_Indefinite_Vectors with
+  SPARK_Mode => Off
+is
 
    function H (New_Item : Element_Type) return Holder renames To_Holder;
    function E (Container : Holder) return Element_Type renames Get;

gcc/ada/a-cfinve.ads

@@ -52,7 +52,9 @@ generic
    --  size, and heap allocation will be avoided. If False, the containers can
    --  grow via heap allocation.
 
-package Ada.Containers.Formal_Indefinite_Vectors is
+package Ada.Containers.Formal_Indefinite_Vectors with
+  SPARK_Mode => On
+is
    pragma Annotate (GNATprove, External_Axiomatization);
 
    subtype Extended_Index is Index_Type'Base
@@ -220,6 +222,7 @@ package Ada.Containers.Formal_Indefinite_Vectors is
      Global => null;
 
 private
+   pragma SPARK_Mode (Off);
 
    pragma Inline (First_Index);
    pragma Inline (Last_Index);

gcc/ada/a-cforma.adb

@@ -34,8 +34,9 @@ pragma Elaborate_All (Ada.Containers.Red_Black_Trees.Generic_Bounded_Keys);
 
 with System; use type System.Address;
 
-package body Ada.Containers.Formal_Ordered_Maps is
+package body Ada.Containers.Formal_Ordered_Maps with
-   pragma SPARK_Mode (Off);
+  SPARK_Mode => Off
+is
 
    -----------------------------
    -- Node Access Subprograms --

gcc/ada/a-cforma.ads

@@ -66,10 +66,11 @@ generic
    with function "<" (Left, Right : Key_Type) return Boolean is <>;
    with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
-package Ada.Containers.Formal_Ordered_Maps is
+package Ada.Containers.Formal_Ordered_Maps with
+  Pure,
+  SPARK_Mode
+is
    pragma Annotate (GNATprove, External_Axiomatization);
-   pragma Pure;
-   pragma SPARK_Mode (On);
 
    function Equivalent_Keys (Left, Right : Key_Type) return Boolean with
      Global => null;
@@ -273,9 +274,10 @@ package Ada.Containers.Formal_Ordered_Maps is
    --  Overlap returns True if the containers have common keys
 
 private
+   pragma SPARK_Mode (Off);
+
    pragma Inline (Next);
    pragma Inline (Previous);
-   pragma SPARK_Mode (Off);
 
    subtype Node_Access is Count_Type;
 

gcc/ada/a-cforse.adb

@@ -38,8 +38,9 @@ pragma Elaborate_All
 
 with System; use type System.Address;
 
-package body Ada.Containers.Formal_Ordered_Sets is
+package body Ada.Containers.Formal_Ordered_Sets with
-   pragma SPARK_Mode (Off);
+  SPARK_Mode => Off
+is
 
    ------------------------------
    -- Access to Fields of Node --

gcc/ada/a-cforse.ads

@@ -64,10 +64,11 @@ generic
    with function "<" (Left, Right : Element_Type) return Boolean is <>;
    with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
-package Ada.Containers.Formal_Ordered_Sets is
+package Ada.Containers.Formal_Ordered_Sets with
+  Pure,
+  SPARK_Mode
+is
    pragma Annotate (GNATprove, External_Axiomatization);
-   pragma Pure;
-   pragma SPARK_Mode (On);
 
    function Equivalent_Elements (Left, Right : Element_Type) return Boolean
    with
@@ -353,9 +354,10 @@ package Ada.Containers.Formal_Ordered_Sets is
    --  scanned yet.
 
 private
+   pragma SPARK_Mode (Off);
+
    pragma Inline (Next);
    pragma Inline (Previous);
-   pragma SPARK_Mode (Off);
 
    type Node_Type is record
       Has_Element : Boolean := False;

gcc/ada/a-cofove.adb

@@ -30,7 +30,9 @@ with Ada.Unchecked_Deallocation;
 
 with System; use type System.Address;
 
-package body Ada.Containers.Formal_Vectors is
+package body Ada.Containers.Formal_Vectors with
+  SPARK_Mode => Off
+is
 
    Growth_Factor : constant := 2;
    --  When growing a container, multiply current capacity by this. Doubling

gcc/ada/a-cofove.ads

@@ -46,7 +46,9 @@ generic
    --  size, and heap allocation will be avoided. If False, the containers can
    --  grow via heap allocation.
 
-package Ada.Containers.Formal_Vectors is
+package Ada.Containers.Formal_Vectors with
+  SPARK_Mode
+is
    pragma Annotate (GNATprove, External_Axiomatization);
 
    subtype Extended_Index is Index_Type'Base
@@ -230,6 +232,7 @@ package Ada.Containers.Formal_Vectors is
    --  scanned yet.
 
 private
+   pragma SPARK_Mode (Off);
 
    pragma Inline (First_Index);
    pragma Inline (Last_Index);

gcc/ada/sem_prag.adb

@@ -14657,6 +14657,12 @@ package body Sem_Prag is
                     (Is_Concurrent_Record_Type (Typ)
                        and then Present (Interfaces (Typ)))
 
+                  --  In analysis-only mode, examine original protected type
+
+                  or else
+                    (Nkind (Parent (Typ)) = N_Protected_Type_Declaration
+                      and then Present (Interface_List (Parent (Typ))))
+
                   --  Check for a private record extension with keyword
                   --  "synchronized".
 

gcc/ada/sem_res.adb

@@ -1794,7 +1794,7 @@ package body Sem_Res is
         and then Nkind (Original_Node (N)) = N_Function_Call
       then
          declare
-            L : constant Node_Id := Left_Opnd  (N);
+            L : Node_Id;
             R : constant Node_Id := Right_Opnd (N);
 
             Old_First : constant Node_Id :=
@@ -1803,7 +1803,8 @@ package body Sem_Res is
 
          begin
             if Is_Binary then
-               Old_Sec   := Next (Old_First);
+               L       := Left_Opnd (N);
+               Old_Sec := Next (Old_First);
 
                --  If the original call has named associations, replace the
                --  explicit actual parameter in the association with the proper

gcc/ada/sem_util.adb

@@ -10846,6 +10846,16 @@ package body Sem_Util is
                          N_Type_Conversion)
       then
          return Is_EVF_Expression (Expression (N));
+
+      --  Attributes 'Loop_Entry, 'Old and 'Update are an EVF expression when
+      --  their prefix denotes an EVF expression.
+
+      elsif Nkind (N) = N_Attribute_Reference
+        and then Nam_In (Attribute_Name (N), Name_Loop_Entry,
+                                             Name_Old,
+                                             Name_Update)
+      then
+         return Is_EVF_Expression (Prefix (N));
       end if;
 
       return False;