[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

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 39c4e09817d9afece11647c2dc65459c653c9aa9..b659777cd8cd43b0a0f8e438c86374d651d64d36 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/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).

diff --git a/gcc/ada/a-cfdlli.adb b/gcc/ada/a-cfdlli.adb
index 993f966f2e1b8bf9086e910497a30f85d478fc41..2fc5d64ad26ccc6972b7c09b5315d9092289e025 100644 (file)
--- a/gcc/ada/a-cfdlli.adb
+++ b/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 --

diff --git a/gcc/ada/a-cfdlli.ads b/gcc/ada/a-cfdlli.ads
index 0c028ef844bbcde54cb33a314820e31b4f65acf2..647d32891e271711f7081f0d6527b757bc6b4d70 100644 (file)
--- a/gcc/ada/a-cfdlli.ads
+++ b/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;

diff --git a/gcc/ada/a-cfhama.adb b/gcc/ada/a-cfhama.adb
index 1780bbb30275e8f057fff6cb557b8fb44d1efe9b..1504f605d71cd3bbe8dde682716ff089626abe63 100644 (file)
--- a/gcc/ada/a-cfhama.adb
+++ b/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
-   pragma SPARK_Mode (Off);
+package body Ada.Containers.Formal_Hashed_Maps with
+  SPARK_Mode => Off
+is
 
    -----------------------
    -- Local Subprograms --

diff --git a/gcc/ada/a-cfhama.ads b/gcc/ada/a-cfhama.ads
index 03a79d8060a9f4121524dc2a094e9ea3b2ce3f36..86e282b3e17c32b79a38ad27d8e9335749455a57 100644 (file)
--- a/gcc/ada/a-cfhama.ads
+++ b/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;

diff --git a/gcc/ada/a-cfhase.adb b/gcc/ada/a-cfhase.adb
index 7c1f9541f6c58b3bf2cc3ba01b66b108bfac274f..3bbcd125776f663afa6a05e670fa98f8b991d550 100644 (file)
--- a/gcc/ada/a-cfhase.adb
+++ b/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
-   pragma SPARK_Mode (Off);
+package body Ada.Containers.Formal_Hashed_Sets with
+  SPARK_Mode => Off
+is
 
    -----------------------
    -- Local Subprograms --

diff --git a/gcc/ada/a-cfhase.ads b/gcc/ada/a-cfhase.ads
index 11018fb57fa1d863fbc2305d766ef892ef72e188..1f802d46c5aa4a66c6a973a3bfdd8a9ffb86f4f7 100644 (file)
--- a/gcc/ada/a-cfhase.ads
+++ b/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;

diff --git a/gcc/ada/a-cfinve.adb b/gcc/ada/a-cfinve.adb
index 793b5c3922f6848c7d0e82c1cd50e306c717da82..e3f917aaa1e6256c8fbc6bd32967cff1e4e0532b 100644 (file)
--- a/gcc/ada/a-cfinve.adb
+++ b/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;

diff --git a/gcc/ada/a-cfinve.ads b/gcc/ada/a-cfinve.ads
index d7600335c5ff0394500608e6a45607ec22127190..b78633b4f8cc0674494af0fcbfd2d562b3c44750 100644 (file)
--- a/gcc/ada/a-cfinve.ads
+++ b/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);

diff --git a/gcc/ada/a-cforma.adb b/gcc/ada/a-cforma.adb
index 8a85cae8fd404b5ca2ce5fbd478508241d646e49..cceef9e11d7a5ad595a21769fc056c84a7a17a8b 100644 (file)
--- a/gcc/ada/a-cforma.adb
+++ b/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
-   pragma SPARK_Mode (Off);
+package body Ada.Containers.Formal_Ordered_Maps with
+  SPARK_Mode => Off
+is
 
    -----------------------------
    -- Node Access Subprograms --

diff --git a/gcc/ada/a-cforma.ads b/gcc/ada/a-cforma.ads
index 5d7827d7e4bc74273bdc7d84760d460d0b216b7c..a20a78904c0ac042367540088ca158e54c41016c 100644 (file)
--- a/gcc/ada/a-cforma.ads
+++ b/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;
 

diff --git a/gcc/ada/a-cforse.adb b/gcc/ada/a-cforse.adb
index 966853a18289441c69a5bdf4204dcae6649f1e33..b53d08c0edf769b522985f8e350083c2835cfc94 100644 (file)
--- a/gcc/ada/a-cforse.adb
+++ b/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
-   pragma SPARK_Mode (Off);
+package body Ada.Containers.Formal_Ordered_Sets with
+  SPARK_Mode => Off
+is
 
    ------------------------------
    -- Access to Fields of Node --

diff --git a/gcc/ada/a-cforse.ads b/gcc/ada/a-cforse.ads
index 081c2b889d06edb39560ddf2bdf154ae5b724ce2..04c66f15c256673048a2e545c2182b4f8d8fcfec 100644 (file)
--- a/gcc/ada/a-cforse.ads
+++ b/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;

diff --git a/gcc/ada/a-cofove.adb b/gcc/ada/a-cofove.adb
index 6776bf90fa28d8640046ce3c91fd9c4a37359b5b..8fc7ed148b6f9898a533670bc4da2f177af7874a 100644 (file)
--- a/gcc/ada/a-cofove.adb
+++ b/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

diff --git a/gcc/ada/a-cofove.ads b/gcc/ada/a-cofove.ads
index 6ac791812b360a0fa9677aa8ac44f594fd91c5f2..5bbd18c2cdd894d866917cc51d7e626caa4f21b0 100644 (file)
--- a/gcc/ada/a-cofove.ads
+++ b/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);

diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index b3e41aa8705407f6752060a0a2df8ad4644b6174..5aa9514d188b3c09affb46105aeb1a88e4fe6c5c 100644 (file)
--- a/gcc/ada/sem_prag.adb
+++ b/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".
 

diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 71f480f4a967a07d0c35af757a24d2d881bae2cc..90311caf969e17c016be962e9614a93ede213f68 100644 (file)
--- a/gcc/ada/sem_res.adb
+++ b/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

diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index dd2ba869f5ce92cf2317592c747ed1177ca3fb35..d29cb7672c2f964f60d4ea5224cd1b766df219a9 100644 (file)
--- a/gcc/ada/sem_util.adb
+++ b/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;