From 5fde9688e077411aa90e1067b8fb9c1d743e4e7f Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Thu, 20 Nov 2014 12:16:44 +0100 Subject: [PATCH] [multiple changes] 2014-11-20 Ed Schonberg * 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 * 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 * sem_util.adb (Is_EVF_Expression): Include attributes 'Loop_Entry, 'Old and 'Update to the logic. 2014-11-20 Bob Duff * 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 | 26 ++++++++++++++++++++++++++ gcc/ada/a-cfdlli.adb | 6 ++++-- gcc/ada/a-cfdlli.ads | 7 +++++-- gcc/ada/a-cfhama.adb | 5 +++-- gcc/ada/a-cfhama.ads | 10 ++++++---- gcc/ada/a-cfhase.adb | 5 +++-- gcc/ada/a-cfhase.ads | 10 ++++++---- gcc/ada/a-cfinve.adb | 4 +++- gcc/ada/a-cfinve.ads | 5 ++++- gcc/ada/a-cforma.adb | 5 +++-- gcc/ada/a-cforma.ads | 10 ++++++---- gcc/ada/a-cforse.adb | 5 +++-- gcc/ada/a-cforse.ads | 10 ++++++---- gcc/ada/a-cofove.adb | 4 +++- gcc/ada/a-cofove.ads | 5 ++++- gcc/ada/sem_prag.adb | 6 ++++++ gcc/ada/sem_res.adb | 5 +++-- gcc/ada/sem_util.adb | 10 ++++++++++ 18 files changed, 104 insertions(+), 34 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 39c4e09817d..b659777cd8c 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,29 @@ +2014-11-20 Ed Schonberg + + * 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 + + * 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 + + * sem_util.adb (Is_EVF_Expression): Include + attributes 'Loop_Entry, 'Old and 'Update to the logic. + +2014-11-20 Bob Duff + + * 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 * initialize.c (ProcListCS): New extern variable (critical section). diff --git a/gcc/ada/a-cfdlli.adb b/gcc/ada/a-cfdlli.adb index 993f966f2e1..2fc5d64ad26 100644 --- 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 0c028ef844b..647d32891e2 100644 --- 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 1780bbb3027..1504f605d71 100644 --- 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 03a79d8060a..86e282b3e17 100644 --- 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 7c1f9541f6c..3bbcd125776 100644 --- 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 11018fb57fa..1f802d46c5a 100644 --- 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 793b5c3922f..e3f917aaa1e 100644 --- a/gcc/ada/a-cfinve.adb +++ b/gcc/ada/a-cfinve.adb @@ -26,7 +26,9 @@ -- . -- ------------------------------------------------------------------------------ -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 d7600335c5f..b78633b4f8c 100644 --- 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 8a85cae8fd4..cceef9e11d7 100644 --- 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 5d7827d7e4b..a20a78904c0 100644 --- 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 966853a1828..b53d08c0edf 100644 --- 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 081c2b889d0..04c66f15c25 100644 --- 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 6776bf90fa2..8fc7ed148b6 100644 --- 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 6ac791812b3..5bbd18c2cdd 100644 --- 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 b3e41aa8705..5aa9514d188 100644 --- 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 71f480f4a96..90311caf969 100644 --- 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 dd2ba869f5c..d29cb7672c2 100644 --- 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; -- 2.30.2