From: Arnaud Charlet Date: Thu, 27 Apr 2017 09:06:47 +0000 (+0200) Subject: [multiple changes] X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=11775988d5f6db984fb902b7447a5b2817b555b1;p=gcc.git [multiple changes] 2017-04-27 Hristian Kirtchev * checks.adb (Generate_Range_Check): Revert previous change. 2017-04-27 Gary Dismukes * sem_util.adb: Minor reformatting/rewording. 2017-04-27 Hristian Kirtchev * lib-xref.adb (Generate_Reference): The use of attribute 'Result is not considered a violation of pragma Unreferenced. 2017-04-27 Justin Squirek * cstand.adb (Create_Standard): Correctly set Directly_Designated_Type for Any_Access. * sem_type.adb (Covers): Minor grammar fixes. 2017-04-27 Bob Duff * sem_attr.adb: Minor cleanup. 2017-04-27 Claire Dross * a-cofuba.ads, a-cofuba.adb (Ada.Containers.Functional_Base): New private child of Ada.Containers used to implement all functional containers. * a-cofuma.ads, a-cofuma.adb (Ada.Containers.Functional_Maps): New child of Ada.Containers. It provides functional indefinite unbounded maps which can be used as high level models for specification of data structures. * a-cofuse.ads, a-cofuse.adb (Ada.Containers.Functional_Sets): New child of Ada.Containers. It provides functional indefinite unbounded sets which can be used as high level models for specification of data structures. * a-cofuve.ads, a-cofuve.adb (Ada.Containers.Functional_Vectors): New child of Ada.Containers. It provides functional indefinite unbounded vectors which can be used as high level models for specification of data structures. * Makefile.rtl: Add new packages. * impunit.adb: Add new packages. From-SVN: r247296 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 1155c406c1b..91c78f8371f 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,47 @@ +2017-04-27 Hristian Kirtchev + + * checks.adb (Generate_Range_Check): Revert previous change. + +2017-04-27 Gary Dismukes + + * sem_util.adb: Minor reformatting/rewording. + +2017-04-27 Hristian Kirtchev + + * lib-xref.adb (Generate_Reference): The use + of attribute 'Result is not considered a violation of pragma + Unreferenced. + +2017-04-27 Justin Squirek + + * cstand.adb (Create_Standard): Correctly set + Directly_Designated_Type for Any_Access. + * sem_type.adb (Covers): Minor grammar fixes. + +2017-04-27 Bob Duff + + * sem_attr.adb: Minor cleanup. + +2017-04-27 Claire Dross + + * a-cofuba.ads, a-cofuba.adb (Ada.Containers.Functional_Base): New + private child of Ada.Containers used to implement all functional + containers. + * a-cofuma.ads, a-cofuma.adb (Ada.Containers.Functional_Maps): New + child of Ada.Containers. It provides functional indefinite unbounded + maps which can be used as high level models for specification + of data structures. + * a-cofuse.ads, a-cofuse.adb (Ada.Containers.Functional_Sets): New + child of Ada.Containers. It provides functional indefinite unbounded + sets which can be used as high level models for specification + of data structures. + * a-cofuve.ads, a-cofuve.adb (Ada.Containers.Functional_Vectors): New + child of Ada.Containers. It provides functional indefinite unbounded + vectors which can be used as high level models for specification + of data structures. + * Makefile.rtl: Add new packages. + * impunit.adb: Add new packages. + 2017-04-27 Gary Dismukes * sem_ch4.adb: Minor reformatting. diff --git a/gcc/ada/Makefile.rtl b/gcc/ada/Makefile.rtl index 63b1a95e3a8..611b09b1b6e 100644 --- a/gcc/ada/Makefile.rtl +++ b/gcc/ada/Makefile.rtl @@ -137,6 +137,10 @@ GNATRTL_NONTASKING_OBJS= \ a-coboho$(objext) \ a-cobove$(objext) \ a-cofove$(objext) \ + a-cofuba$(objext) \ + a-cofuma$(objext) \ + a-cofuse$(objext) \ + a-cofuve$(objext) \ a-cogeso$(objext) \ a-cohama$(objext) \ a-cohase$(objext) \ diff --git a/gcc/ada/a-cofuba.adb b/gcc/ada/a-cofuba.adb new file mode 100644 index 00000000000..dd29eea2f56 --- /dev/null +++ b/gcc/ada/a-cofuba.adb @@ -0,0 +1,206 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT LIBRARY COMPONENTS -- +-- -- +-- ADA.CONTAINERS.FUNCTIONAL_BASE -- +-- -- +-- B o d y -- +-- -- +-- Copyright (C) 2016-2017, Free Software Foundation, Inc. -- +-- -- +-- This specification is derived from the Ada Reference Manual for use with -- +-- GNAT. The copyright notice above, and the license provisions that follow -- +-- apply solely to the contents of the part following the private keyword. -- +-- -- +-- 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- -- +-- ware Foundation; either version 3, or (at your option) any later ver- -- +-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- +-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- +-- or FITNESS FOR A PARTICULAR PURPOSE. -- +-- -- +-- As a special exception under Section 7 of GPL version 3, you are granted -- +-- additional permissions described in the GCC Runtime Library Exception, -- +-- version 3.1, as published by the Free Software Foundation. -- +-- -- +-- You should have received a copy of the GNU General Public License and -- +-- a copy of the GCC Runtime Library Exception along with this program; -- +-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- +-- . -- +------------------------------------------------------------------------------ + +pragma Ada_2012; + +package body Ada.Containers.Functional_Base with SPARK_Mode => Off is + + pragma Assertion_Policy + (Pre => Suppressible, Ghost => Suppressible, Post => Ignore); + + function To_Count (Idx : Extended_Index) return Count_Type + is (Count_Type + (Extended_Index'Pos (Idx) + - Extended_Index'Pos (Extended_Index'First))); + function To_Index (Position : Count_Type) return Extended_Index + is (Extended_Index'Val + (Position + + Extended_Index'Pos (Extended_Index'First))); + -- Conversion functions between Index_Type and Count_Type + + function Find (C : Container; E : access Element_Type) return Count_Type; + -- Search a container C for an element equal to E.all, return the + -- position in the underlying array. + + --------- + -- "=" -- + --------- + + function "=" (C1, C2 : Container) return Boolean is + begin + if C1.Elements'Length /= C2.Elements'Length then + return False; + end if; + + for I in C1.Elements'Range loop + if C1.Elements (I).all /= C2.Elements (I).all then + return False; + end if; + end loop; + return True; + end "="; + + ---------- + -- "<=" -- + ---------- + + function "<=" (C1, C2 : Container) return Boolean is + begin + for I in C1.Elements'Range loop + if Find (C2, C1.Elements (I)) = 0 then + return False; + end if; + end loop; + return True; + end "<="; + + --------- + -- Add -- + --------- + + function Add (C : Container; E : Element_Type) return Container is + begin + return Container'(Elements => + new Element_Array' + (C.Elements.all & new Element_Type'(E))); + end Add; + + ---------- + -- Find -- + ---------- + + function Find (C : Container; E : access Element_Type) return Count_Type is + begin + for I in C.Elements'Range loop + if C.Elements (I).all = E.all then + return I; + end if; + end loop; + return 0; + end Find; + + function Find (C : Container; E : Element_Type) return Extended_Index is + (To_Index (Find (C, E'Unrestricted_Access))); + + --------- + -- Get -- + --------- + + function Get (C : Container; I : Index_Type) return Element_Type is + (C.Elements (To_Count (I)).all); + + ------------------ + -- Intersection -- + ------------------ + + function Intersection (C1, C2 : Container) return Container is + A : constant Element_Array_Access := + new Element_Array'(1 .. Num_Overlaps (C1, C2) => <>); + P : Count_Type := 0; + begin + for I in C1.Elements'Range loop + if Find (C2, C1.Elements (I)) > 0 then + P := P + 1; + A (P) := C1.Elements (I); + end if; + end loop; + return Container'(Elements => A); + end Intersection; + + ------------ + -- Length -- + ------------ + + function Length (C : Container) return Count_Type is + (C.Elements'Length); + + --------------------- + -- Num_Overlaps -- + --------------------- + + function Num_Overlaps (C1, C2 : Container) return Count_Type is + P : Count_Type := 0; + begin + for I in C1.Elements'Range loop + if Find (C2, C1.Elements (I)) > 0 then + P := P + 1; + end if; + end loop; + return P; + end Num_Overlaps; + + --------- + -- Set -- + --------- + + function Set (C : Container; I : Index_Type; E : Element_Type) + return Container + is + Result : constant Container := + Container'(Elements => new Element_Array'(C.Elements.all)); + begin + Result.Elements (To_Count (I)) := new Element_Type'(E); + return Result; + end Set; + + ----------- + -- Union -- + ----------- + + function Union (C1, C2 : Container) return Container is + N : constant Count_Type := Num_Overlaps (C1, C2); + + begin + -- if C2 is completely included in C1 then return C1 + + if N = Length (C2) then + return C1; + end if; + + -- else loop through C2 to find the remaining elements + + declare + L : constant Count_Type := Length (C1) - N + Length (C2); + A : constant Element_Array_Access := + new Element_Array'(C1.Elements.all & (Length (C1) + 1 .. L => <>)); + P : Count_Type := Length (C1); + begin + for I in C2.Elements'Range loop + if Find (C1, C2.Elements (I)) = 0 then + P := P + 1; + A (P) := C2.Elements (I); + end if; + end loop; + return Container'(Elements => A); + end; + end Union; + +end Ada.Containers.Functional_Base; diff --git a/gcc/ada/a-cofuba.ads b/gcc/ada/a-cofuba.ads new file mode 100644 index 00000000000..6bcea9d2022 --- /dev/null +++ b/gcc/ada/a-cofuba.ads @@ -0,0 +1,104 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT LIBRARY COMPONENTS -- +-- -- +-- ADA.CONTAINERS.FUNCTIONAL_BASE -- +-- -- +-- S p e c -- +-- -- +-- Copyright (C) 2016-2017, Free Software Foundation, Inc. -- +-- -- +-- This specification is derived from the Ada Reference Manual for use with -- +-- GNAT. The copyright notice above, and the license provisions that follow -- +-- apply solely to the contents of the part following the private keyword. -- +-- -- +-- 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- -- +-- ware Foundation; either version 3, or (at your option) any later ver- -- +-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- +-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- +-- or FITNESS FOR A PARTICULAR PURPOSE. -- +-- -- +-- As a special exception under Section 7 of GPL version 3, you are granted -- +-- additional permissions described in the GCC Runtime Library Exception, -- +-- version 3.1, as published by the Free Software Foundation. -- +-- -- +-- You should have received a copy of the GNU General Public License and -- +-- a copy of the GCC Runtime Library Exception along with this program; -- +-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- +-- . -- +------------------------------------------------------------------------------ +-- Functional containers are neither controlled nor limited. This is safe as +-- no primitives is provided to modify them. +-- Memory allocated inside functional containers is never reclaimed. + +pragma Ada_2012; + +private generic + type Index_Type is (<>); + -- To avoid Constraint_Error being raised at runtime, Index_Type'Base + -- should have at least one more element at the left than Index_Type. + + type Element_Type (<>) is private; + with function "=" (Left, Right : Element_Type) return Boolean is <>; +package Ada.Containers.Functional_Base with SPARK_Mode => Off is + + subtype Extended_Index is Index_Type'Base range + Index_Type'Pred (Index_Type'First) .. Index_Type'Last; + + type Container is private; + + function "=" (C1, C2 : Container) return Boolean; + -- Return True if C1 and C2 contain the same elements at the same position + + function Length (C : Container) return Count_Type; + -- Number of elements stored in C. + + function Get (C : Container; I : Index_Type) return Element_Type; + -- Access to the element at index I in C. + + function Set (C : Container; I : Index_Type; E : Element_Type) + return Container; + -- Return a new container which is equal to C except for the element at + -- index I which is set to E. + + function Add (C : Container; E : Element_Type) return Container; + -- Return a new container which is C appended with E. + + function Find (C : Container; E : Element_Type) return Extended_Index; + -- Return the first index for which the element stored in C is I. + -- If there are no such indexes, return Extended_Index'First. + + -------------------- + -- Set Operations -- + -------------------- + + function "<=" (C1, C2 : Container) return Boolean; + -- Return True if every element of C1 is in C2 + + function Num_Overlaps (C1, C2 : Container) return Count_Type; + -- Return the number of elements that are both in + + function Union (C1, C2 : Container) return Container; + -- Return a container which is C1 plus all the elements of C2 that are not + -- in C1. + + function Intersection (C1, C2 : Container) return Container; + -- Return a container which is C1 minus all the elements that are also in + -- C2. + +private + + subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last; + + type Element_Access is access all Element_Type; + type Element_Array is + array (Positive_Count_Type range <>) of Element_Access; + type Element_Array_Access is not null access Element_Array; + Empty_Element_Array_Access : constant Element_Array_Access := + new Element_Array'(1 .. 0 => null); + + type Container is record + Elements : Element_Array_Access := Empty_Element_Array_Access; + end record; +end Ada.Containers.Functional_Base; diff --git a/gcc/ada/a-cofuma.adb b/gcc/ada/a-cofuma.adb new file mode 100644 index 00000000000..9367baeea13 --- /dev/null +++ b/gcc/ada/a-cofuma.adb @@ -0,0 +1,161 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT LIBRARY COMPONENTS -- +-- -- +-- ADA.CONTAINERS.FUNCTIONAL_MAPS -- +-- -- +-- B o d y -- +-- -- +-- Copyright (C) 2016-2017, Free Software Foundation, Inc. -- +-- -- +-- This specification is derived from the Ada Reference Manual for use with -- +-- GNAT. The copyright notice above, and the license provisions that follow -- +-- apply solely to the contents of the part following the private keyword. -- +-- -- +-- 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- -- +-- ware Foundation; either version 3, or (at your option) any later ver- -- +-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- +-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- +-- or FITNESS FOR A PARTICULAR PURPOSE. -- +-- -- +-- As a special exception under Section 7 of GPL version 3, you are granted -- +-- additional permissions described in the GCC Runtime Library Exception, -- +-- version 3.1, as published by the Free Software Foundation. -- +-- -- +-- You should have received a copy of the GNU General Public License and -- +-- a copy of the GCC Runtime Library Exception along with this program; -- +-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- +-- . -- +------------------------------------------------------------------------------ + +pragma Ada_2012; +package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is + use Key_Containers; + use Element_Containers; + + pragma Assertion_Policy + (Pre => Suppressible, Ghost => Suppressible, Post => Ignore); + + --------- + -- "=" -- + --------- + + function "=" (M1, M2 : Map) return Boolean is + (M1.Keys <= M2.Keys and M2 <= M1); + + ---------- + -- "<=" -- + ---------- + + function "<=" (M1, M2 : Map) return Boolean is + I2 : Count_Type; + begin + for I1 in 1 .. Length (M1.Keys) loop + I2 := Find (M2.Keys, Get (M1.Keys, I1)); + if I2 = 0 + or else Get (M2.Elements, I2) /= Get (M1.Elements, I1) + then + return False; + end if; + end loop; + return True; + end "<="; + + --------- + -- Add -- + --------- + + function Add (M : Map; K : Key_Type; E : Element_Type) return Map is + begin + return + (Keys => Add (M.Keys, K), + Elements => Add (M.Elements, E)); + end Add; + + --------- + -- Get -- + --------- + + function Get (M : Map; K : Key_Type) return Element_Type is + begin + return Get (M.Elements, Find (M.Keys, K)); + end Get; + + ------------ + -- Is_Add -- + ------------ + + function Is_Add + (M : Map; K : Key_Type; E : Element_Type; Result : Map) return Boolean + is + begin + if Mem (M, K) or not Mem (Result, K) or Get (Result, K) /= E then + return False; + end if; + + for K of M loop + if not Mem (Result, K) or else Get (Result, K) /= Get (M, K) then + return False; + end if; + end loop; + + for KK of Result loop + if KK /= K and not Mem (M, KK) then + return False; + end if; + end loop; + + return True; + end Is_Add; + + -------------- + -- Is_Empty -- + -------------- + + function Is_Empty (M : Map) return Boolean is + begin + return Length (M.Keys) = 0; + end Is_Empty; + + ------------ + -- Is_Set -- + ------------ + + function Is_Set + (M : Map; K : Key_Type; E : Element_Type; Result : Map) return Boolean + is + (Mem (M, K) + and then Mem (Result, K) + and then Get (Result, K) = E + and then (for all KK of M => Mem (Result, KK) + and then + (if K /= KK + then Get (Result, KK) = Get (M, KK))) + and then (for all K of Result => Mem (M, K))); + + ------------ + -- Length -- + ------------ + + function Length (M : Map) return Count_Type is + begin + return Length (M.Elements); + end Length; + + --------- + -- Mem -- + --------- + + function Mem (M : Map; K : Key_Type) return Boolean is + begin + return Find (M.Keys, K) > 0; + end Mem; + + --------- + -- Set -- + --------- + + function Set (M : Map; K : Key_Type; E : Element_Type) return Map is + (Keys => M.Keys, Elements => Set (M.Elements, Find (M.Keys, K), E)); +end Ada.Containers.Functional_Maps; diff --git a/gcc/ada/a-cofuma.ads b/gcc/ada/a-cofuma.ads new file mode 100644 index 00000000000..23fb45c0a9d --- /dev/null +++ b/gcc/ada/a-cofuma.ads @@ -0,0 +1,193 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT LIBRARY COMPONENTS -- +-- -- +-- ADA.CONTAINERS.FUNCTIONAL_MAPS -- +-- -- +-- S p e c -- +-- -- +-- Copyright (C) 2016-2017, Free Software Foundation, Inc. -- +-- -- +-- This specification is derived from the Ada Reference Manual for use with -- +-- GNAT. The copyright notice above, and the license provisions that follow -- +-- apply solely to the contents of the part following the private keyword. -- +-- -- +-- 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- -- +-- ware Foundation; either version 3, or (at your option) any later ver- -- +-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- +-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- +-- or FITNESS FOR A PARTICULAR PURPOSE. -- +-- -- +-- As a special exception under Section 7 of GPL version 3, you are granted -- +-- additional permissions described in the GCC Runtime Library Exception, -- +-- version 3.1, as published by the Free Software Foundation. -- +-- -- +-- You should have received a copy of the GNU General Public License and -- +-- a copy of the GCC Runtime Library Exception along with this program; -- +-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- +-- . -- +------------------------------------------------------------------------------ + +pragma Ada_2012; +private with Ada.Containers.Functional_Base; + +generic + type Key_Type (<>) is private; + type Element_Type (<>) is private; + with function Equivalent_Keys (Left, Right : Key_Type) return Boolean; + with function "=" (Left, Right : Element_Type) return Boolean is <>; +package Ada.Containers.Functional_Maps with SPARK_Mode is + + type Map is private with + Default_Initial_Condition => Is_Empty (Map) and Length (Map) = 0, + Iterable => (First => Iter_First, + Next => Iter_Next, + Has_Element => Iter_Has_Element, + Element => Iter_Element); + -- Maps are empty when default initialized. + -- For in quantification over maps should not be used. + -- For of quantification over maps iterates over keys. + + -- Maps are axiomatized using Mem and Get encoding respectively the + -- presence of a key in a map and an accessor to elements associated to its + -- keys. The length of a map is also added to protect Add against overflows + -- but it is not actually modeled. + + function Mem (M : Map; K : Key_Type) return Boolean with + Global => null; + function Get (M : Map; K : Key_Type) return Element_Type with + Global => null, + Pre => Mem (M, K); + + function Length (M : Map) return Count_Type with + Global => null; + + function "<=" (M1, M2 : Map) return Boolean with + -- Map inclusion. + + Global => null, + Post => "<="'Result = + (for all K of M1 => Mem (M2, K) + and then Get (M2, K) = Get (M1, K)); + + function "=" (M1, M2 : Map) return Boolean with + -- Extensional equality over maps. + + Global => null, + Post => "="'Result = + ((for all K of M1 => Mem (M2, K) + and then Get (M2, K) = Get (M1, K)) + and (for all K of M2 => Mem (M1, K))); + + pragma Warnings (Off, "unused variable ""K"""); + function Is_Empty (M : Map) return Boolean with + -- A map is empty if it contains no key. + + Global => null, + Post => Is_Empty'Result = (for all K of M => False); + pragma Warnings (On, "unused variable ""K"""); + + function Is_Add + (M : Map; K : Key_Type; E : Element_Type; Result : Map) return Boolean + -- Returns True if Result is M augmented with the mapping K -> E. + + with + Global => null, + Post => Is_Add'Result = + (not Mem (M, K) + and then (Mem (Result, K) and then Get (Result, K) = E + and then (for all K of M => Mem (Result, K) + and then Get (Result, K) = Get (M, K)) + and then (for all KK of Result => + Equivalent_Keys (KK, K) or Mem (M, KK)))); + + function Add (M : Map; K : Key_Type; E : Element_Type) return Map with + -- Returns M augmented with the mapping K -> E. + -- Is_Add (M, K, E, Result) should be used instead of + -- Result = Add (M, K, E) whenever possible both for execution and for + -- proof. + + Global => null, + Pre => not Mem (M, K) and Length (M) < Count_Type'Last, + Post => Length (M) + 1 = Length (Add'Result) + and Is_Add (M, K, E, Add'Result); + + function Is_Set + (M : Map; K : Key_Type; E : Element_Type; Result : Map) return Boolean + -- Returns True if Result is M where the element associated to K has been + -- replaced by E. + + with + Global => null, + Post => Is_Set'Result = + (Mem (M, K) + and then Mem (Result, K) + and then Get (Result, K) = E + and then (for all KK of M => Mem (Result, KK) + and then (if not Equivalent_Keys (K, KK) + then Get (Result, KK) = Get (M, KK))) + and then (for all K of Result => Mem (M, K))); + + function Set (M : Map; K : Key_Type; E : Element_Type) return Map with + -- Returns M where the element associated to K has been replaced by E. + -- Is_Set (M, K, E, Result) should be used instead of + -- Result = Set (M, K, E) whenever possible both for execution and for + -- proof. + + Global => null, + Pre => Mem (M, K), + Post => Length (M) = Length (Set'Result) + and Is_Set (M, K, E, Set'Result); + + --------------------------- + -- Iteration Primitives -- + --------------------------- + + type Private_Key is private; + + function Iter_First (M : Map) return Private_Key with + Global => null; + function Iter_Has_Element (M : Map; K : Private_Key) return Boolean with + Global => null; + function Iter_Next (M : Map; K : Private_Key) return Private_Key with + Global => null, + Pre => Iter_Has_Element (M, K); + function Iter_Element (M : Map; K : Private_Key) return Key_Type with + Global => null, + Pre => Iter_Has_Element (M, K); + pragma Annotate (GNATprove, Iterable_For_Proof, "Contains", Mem); +private + pragma SPARK_Mode (Off); + + function "=" (Left, Right : Key_Type) return Boolean + renames Equivalent_Keys; + + subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last; + + package Element_Containers is new Ada.Containers.Functional_Base + (Element_Type => Element_Type, + Index_Type => Positive_Count_Type); + + package Key_Containers is new Ada.Containers.Functional_Base + (Element_Type => Key_Type, + Index_Type => Positive_Count_Type); + + type Map is record + Keys : Key_Containers.Container; + Elements : Element_Containers.Container; + end record; + + type Private_Key is new Count_Type; + + function Iter_First (M : Map) return Private_Key is (1); + + function Iter_Has_Element (M : Map; K : Private_Key) return Boolean is + (Count_Type (K) in 1 .. Key_Containers.Length (M.Keys)); + + function Iter_Next (M : Map; K : Private_Key) return Private_Key is + (if K = Private_Key'Last then 0 else K + 1); + + function Iter_Element (M : Map; K : Private_Key) return Key_Type is + (Key_Containers.Get (M.Keys, Count_Type (K))); +end Ada.Containers.Functional_Maps; diff --git a/gcc/ada/a-cofuse.adb b/gcc/ada/a-cofuse.adb new file mode 100644 index 00000000000..21417b2eda7 --- /dev/null +++ b/gcc/ada/a-cofuse.adb @@ -0,0 +1,128 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT LIBRARY COMPONENTS -- +-- -- +-- ADA.CONTAINERS.FUNCTIONAL_SETS -- +-- -- +-- B o d y -- +-- -- +-- Copyright (C) 2016-2017, Free Software Foundation, Inc. -- +-- -- +-- This specification is derived from the Ada Reference Manual for use with -- +-- GNAT. The copyright notice above, and the license provisions that follow -- +-- apply solely to the contents of the part following the private keyword. -- +-- -- +-- 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- -- +-- ware Foundation; either version 3, or (at your option) any later ver- -- +-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- +-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- +-- or FITNESS FOR A PARTICULAR PURPOSE. -- +-- -- +-- As a special exception under Section 7 of GPL version 3, you are granted -- +-- additional permissions described in the GCC Runtime Library Exception, -- +-- version 3.1, as published by the Free Software Foundation. -- +-- -- +-- You should have received a copy of the GNU General Public License and -- +-- a copy of the GCC Runtime Library Exception along with this program; -- +-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- +-- . -- +------------------------------------------------------------------------------ + +pragma Ada_2012; + +package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is + use Containers; + + pragma Assertion_Policy + (Pre => Suppressible, Ghost => Suppressible, Post => Ignore); + + --------- + -- "=" -- + --------- + + function "=" (S1, S2 : Set) return Boolean is + (S1.Content <= S2.Content and S2.Content <= S1.Content); + + ---------- + -- "<=" -- + ---------- + + function "<=" (S1, S2 : Set) return Boolean is (S1.Content <= S2.Content); + + --------- + -- Add -- + --------- + + function Add (S : Set; E : Element_Type) return Set is + (Content => Add (S.Content, E)); + + ------------ + -- Length -- + ------------ + + function Length (S : Set) return Count_Type is (Length (S.Content)); + + --------- + -- Mem -- + --------- + + function Mem (S : Set; E : Element_Type) return Boolean is + (Find (S.Content, E) > 0); + + ------------------ + -- Num_Overlaps -- + ------------------ + + function Num_Overlaps (S1, S2 : Set) return Count_Type is + (Num_Overlaps (S1.Content, S2.Content)); + + ------------------ + -- Intersection -- + ------------------ + + function Intersection (S1, S2 : Set) return Set is + (Content => Intersection (S1.Content, S2.Content)); + + ------------ + -- Is_Add -- + ------------ + + function Is_Add (S : Set; E : Element_Type; Result : Set) return Boolean + is + (Mem (Result, E) + and (for all F of Result => Mem (S, F) or F = E) + and (for all E of S => Mem (Result, E))); + + -------------- + -- Is_Empty -- + -------------- + + function Is_Empty (S : Set) return Boolean is (Length (S.Content) = 0); + + --------------------- + -- Is_Intersection -- + --------------------- + + function Is_Intersection (S1, S2, Result : Set) return Boolean is + ((for all E of Result => + Mem (S1, E) and Mem (S2, E)) + and (for all E of S1 => + (if Mem (S2, E) then Mem (Result, E)))); + + -------------- + -- Is_Union -- + -------------- + + function Is_Union (S1, S2, Result : Set) return Boolean is + ((for all E of Result => Mem (S1, E) or Mem (S2, E)) + and (for all E of S1 => Mem (Result, E)) + and (for all E of S2 => Mem (Result, E))); + + ----------- + -- Union -- + ----------- + + function Union (S1, S2 : Set) return Set is + (Content => Union (S1.Content, S2.Content)); +end Ada.Containers.Functional_Sets; diff --git a/gcc/ada/a-cofuse.ads b/gcc/ada/a-cofuse.ads new file mode 100644 index 00000000000..cbc03fa8e04 --- /dev/null +++ b/gcc/ada/a-cofuse.ads @@ -0,0 +1,195 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT LIBRARY COMPONENTS -- +-- -- +-- ADA.CONTAINERS.FUNCTIONAL_SETS -- +-- -- +-- S p e c -- +-- -- +-- Copyright (C) 2016-2017, Free Software Foundation, Inc. -- +-- -- +-- This specification is derived from the Ada Reference Manual for use with -- +-- GNAT. The copyright notice above, and the license provisions that follow -- +-- apply solely to the contents of the part following the private keyword. -- +-- -- +-- 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- -- +-- ware Foundation; either version 3, or (at your option) any later ver- -- +-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- +-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- +-- or FITNESS FOR A PARTICULAR PURPOSE. -- +-- -- +-- As a special exception under Section 7 of GPL version 3, you are granted -- +-- additional permissions described in the GCC Runtime Library Exception, -- +-- version 3.1, as published by the Free Software Foundation. -- +-- -- +-- You should have received a copy of the GNU General Public License and -- +-- a copy of the GCC Runtime Library Exception along with this program; -- +-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- +-- . -- +------------------------------------------------------------------------------ + +pragma Ada_2012; +private with Ada.Containers.Functional_Base; + +generic + type Element_Type (<>) is private; + with function "=" (Left, Right : Element_Type) return Boolean is <>; +package Ada.Containers.Functional_Sets with SPARK_Mode is + + type Set is private with + Default_Initial_Condition => Is_Empty (Set) and Length (Set) = 0, + Iterable => (First => Iter_First, + Next => Iter_Next, + Has_Element => Iter_Has_Element, + Element => Iter_Element); + -- Sets are empty when default initialized. + -- For in quantification over sets should not be used. + -- For of quantification over sets iterates over elements. + + -- Sets are axiomatized using Mem which encodes whether an element is + -- contained in a set. The length of a set is also added to protect Add + -- against overflows but it is not actually modeled. + + function Mem (S : Set; E : Element_Type) return Boolean with + Global => null; + + function Length (S : Set) return Count_Type with + Global => null; + + function "<=" (S1, S2 : Set) return Boolean with + -- Set inclusion. + + Global => null, + Post => "<="'Result = (for all E of S1 => Mem (S2, E)); + + function "=" (S1, S2 : Set) return Boolean with + -- Extensional equality over sets. + + Global => null, + Post => + "="'Result = ((for all E of S1 => Mem (S2, E)) + and (for all E of S2 => Mem (S1, E))); + + pragma Warnings (Off, "unused variable ""E"""); + function Is_Empty (S : Set) return Boolean with + -- A set is empty if it contains no element. + + Global => null, + Post => Is_Empty'Result = (for all E of S => False); + pragma Warnings (On, "unused variable ""E"""); + + function Is_Add (S : Set; E : Element_Type; Result : Set) return Boolean + -- Returns True if Result is S augmented with E. + + with + Global => null, + Post => Is_Add'Result = + (Mem (Result, E) and not Mem (S, E) + and (for all F of Result => Mem (S, F) or F = E) + and (for all E of S => Mem (Result, E))); + + function Add (S : Set; E : Element_Type) return Set with + -- Returns S augmented with E. + -- Is_Add (S, E, Result) should be used instead of Result = Add (S, E) + -- whenever possible both for execution and for proof. + + Global => null, + Pre => not Mem (S, E) and Length (S) < Count_Type'Last, + Post => Length (Add'Result) = Length (S) + 1 + and Is_Add (S, E, Add'Result); + + function Is_Intersection (S1, S2, Result : Set) return Boolean with + -- Returns True if Result is the intersection of S1 and S2. + + Global => null, + Post => Is_Intersection'Result = + ((for all E of Result => + Mem (S1, E) and Mem (S2, E)) + and (for all E of S1 => + (if Mem (S2, E) then Mem (Result, E)))); + + function Num_Overlaps (S1, S2 : Set) return Count_Type with + -- Number of elements that are both in S1 and S2. + + Global => null, + Post => Num_Overlaps'Result <= Length (S1) + and Num_Overlaps'Result <= Length (S2) + and (if Num_Overlaps'Result = 0 then + (for all E of S1 => not Mem (S2, E))); + + function Intersection (S1, S2 : Set) return Set with + -- Returns the intersection of S1 and S2. + -- Intersection (S1, S2, Result) should be used instead of + -- Result = Intersection (S1, S2) whenever possible both for execution and + -- for proof. + + Global => null, + Post => Length (Intersection'Result) = Num_Overlaps (S1, S2) + and Is_Intersection (S1, S2, Intersection'Result); + + function Is_Union (S1, S2, Result : Set) return Boolean with + -- Returns True if Result is the union of S1 and S2. + + Global => null, + Post => Is_Union'Result = + ((for all E of Result => Mem (S1, E) or Mem (S2, E)) + and (for all E of S1 => Mem (Result, E)) + and (for all E of S2 => Mem (Result, E))); + + function Union (S1, S2 : Set) return Set with + -- Returns the union of S1 and S2. + -- Is_Union (S1, S2, Result) should be used instead of + -- Result = Union (S1, S2) whenever possible both for execution and for + -- proof. + + Global => null, + Pre => Length (S1) - Num_Overlaps (S1, S2) <= + Count_Type'Last - Length (S2), + Post => Length (Union'Result) = Length (S1) - Num_Overlaps (S1, S2) + + Length (S2) + and Is_Union (S1, S2, Union'Result); + + --------------------------- + -- Iteration Primitives -- + --------------------------- + + type Private_Key is private; + + function Iter_First (S : Set) return Private_Key with + Global => null; + function Iter_Has_Element (S : Set; K : Private_Key) return Boolean with + Global => null; + function Iter_Next (S : Set; K : Private_Key) return Private_Key with + Global => null, + Pre => Iter_Has_Element (S, K); + function Iter_Element (S : Set; K : Private_Key) return Element_Type with + Global => null, + Pre => Iter_Has_Element (S, K); + pragma Annotate (GNATprove, Iterable_For_Proof, "Contains", Mem); +private + pragma SPARK_Mode (Off); + + subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last; + + package Containers is new Ada.Containers.Functional_Base + (Element_Type => Element_Type, + Index_Type => Positive_Count_Type); + + type Set is record + Content : Containers.Container; + end record; + + type Private_Key is new Count_Type; + + function Iter_First (S : Set) return Private_Key is (1); + + function Iter_Has_Element (S : Set; K : Private_Key) return Boolean is + (Count_Type (K) in 1 .. Containers.Length (S.Content)); + + function Iter_Next (S : Set; K : Private_Key) return Private_Key is + (if K = Private_Key'Last then 0 else K + 1); + + function Iter_Element (S : Set; K : Private_Key) return Element_Type is + (Containers.Get (S.Content, Count_Type (K))); +end Ada.Containers.Functional_Sets; diff --git a/gcc/ada/a-cofuve.adb b/gcc/ada/a-cofuve.adb new file mode 100644 index 00000000000..6f4f2b131b6 --- /dev/null +++ b/gcc/ada/a-cofuve.adb @@ -0,0 +1,133 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT LIBRARY COMPONENTS -- +-- -- +-- ADA.CONTAINERS.FUNCTIONAL_VECTORS -- +-- -- +-- B o d y -- +-- -- +-- Copyright (C) 2016-2017, Free Software Foundation, Inc. -- +-- -- +-- This specification is derived from the Ada Reference Manual for use with -- +-- GNAT. The copyright notice above, and the license provisions that follow -- +-- apply solely to the contents of the part following the private keyword. -- +-- -- +-- 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- -- +-- ware Foundation; either version 3, or (at your option) any later ver- -- +-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- +-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- +-- or FITNESS FOR A PARTICULAR PURPOSE. -- +-- -- +-- As a special exception under Section 7 of GPL version 3, you are granted -- +-- additional permissions described in the GCC Runtime Library Exception, -- +-- version 3.1, as published by the Free Software Foundation. -- +-- -- +-- You should have received a copy of the GNU General Public License and -- +-- a copy of the GCC Runtime Library Exception along with this program; -- +-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- +-- . -- +------------------------------------------------------------------------------ + +pragma Ada_2012; +package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is + use Containers; + + pragma Assertion_Policy + (Pre => Suppressible, Ghost => Suppressible, Post => Ignore); + + --------- + -- "=" -- + --------- + + function "=" (S1, S2 : Sequence) return Boolean is + (S1.Content = S2.Content); + + --------- + -- "<" -- + --------- + + function "<" (S1, S2 : Sequence) return Boolean is + (Length (S1.Content) < Length (S2.Content) + and then (for all I in Index_Type'First .. Last (S1) => + Get (S1.Content, I) = Get (S2.Content, I))); + + ---------- + -- "<=" -- + ---------- + + function "<=" (S1, S2 : Sequence) return Boolean is + (Length (S1.Content) <= Length (S2.Content) + and then (for all I in Index_Type'First .. Last (S1) => + Get (S1.Content, I) = Get (S2.Content, I))); + + --------- + -- Add -- + --------- + + function Add (S : Sequence; E : Element_Type) return Sequence is + (Content => Add (S.Content, E)); + + --------- + -- Get -- + --------- + + function Get (S : Sequence; N : Extended_Index) return Element_Type is + (Get (S.Content, N)); + + ------------ + -- Is_Add -- + ------------ + + function Is_Add + (S : Sequence; E : Element_Type; Result : Sequence) return Boolean is + (Length (Result) = Length (S) + 1 + and then Get (Result, Index_Type'Val + ((Index_Type'Pos (Index_Type'First) - 1) + + Length (Result))) = E + and then + (for all M in Index_Type'First .. + (Index_Type'Val + ((Index_Type'Pos (Index_Type'First) - 1) + Length (S))) => + Get (Result, M) = Get (S, M))); + + ------------ + -- Is_Set -- + ------------ + + function Is_Set + (S : Sequence; N : Index_Type; E : Element_Type; Result : Sequence) + return Boolean is + (N in Index_Type'First .. + (Index_Type'Val + ((Index_Type'Pos (Index_Type'First) - 1) + Length (S))) + and then Length (Result) = Length (S) + and then Get (Result, N) = E + and then + (for all M in Index_Type'First .. + (Index_Type'Val + ((Index_Type'Pos (Index_Type'First) - 1) + Length (S))) => + (if M /= N then Get (Result, M) = Get (S, M)))); + + ---------- + -- Last -- + ---------- + + function Last (S : Sequence) return Extended_Index is + (Index_Type'Val ((Index_Type'Pos (Index_Type'First) - 1) + Length (S))); + + ------------ + -- Length -- + ------------ + + function Length (S : Sequence) return Count_Type is + (Length (S.Content)); + + --------- + -- Set -- + --------- + + function Set (S : Sequence; N : Index_Type; E : Element_Type) + return Sequence is + (Content => Set (S.Content, N, E)); +end Ada.Containers.Functional_Vectors; diff --git a/gcc/ada/a-cofuve.ads b/gcc/ada/a-cofuve.ads new file mode 100644 index 00000000000..9d990a9afc3 --- /dev/null +++ b/gcc/ada/a-cofuve.ads @@ -0,0 +1,198 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT LIBRARY COMPONENTS -- +-- -- +-- ADA.CONTAINERS.FUNCTIONAL_VECTORS -- +-- -- +-- S p e c -- +-- -- +-- Copyright (C) 2016-2017, Free Software Foundation, Inc. -- +-- -- +-- This specification is derived from the Ada Reference Manual for use with -- +-- GNAT. The copyright notice above, and the license provisions that follow -- +-- apply solely to the contents of the part following the private keyword. -- +-- -- +-- 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- -- +-- ware Foundation; either version 3, or (at your option) any later ver- -- +-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- +-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- +-- or FITNESS FOR A PARTICULAR PURPOSE. -- +-- -- +-- As a special exception under Section 7 of GPL version 3, you are granted -- +-- additional permissions described in the GCC Runtime Library Exception, -- +-- version 3.1, as published by the Free Software Foundation. -- +-- -- +-- You should have received a copy of the GNU General Public License and -- +-- a copy of the GCC Runtime Library Exception along with this program; -- +-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- +-- . -- +------------------------------------------------------------------------------ + +pragma Ada_2012; +private with Ada.Containers.Functional_Base; + +generic + type Index_Type is (<>); + -- To avoid Constraint_Error being raised at runtime, Index_Type'Base + -- should have at least one more element at the left than Index_Type. + + type Element_Type (<>) is private; + with function "=" (Left, Right : Element_Type) return Boolean is <>; +package Ada.Containers.Functional_Vectors with SPARK_Mode is + + subtype Extended_Index is Index_Type'Base range + Index_Type'Pred (Index_Type'First) .. Index_Type'Last; + -- Index_Type with one more element to the left. + -- This type is never used but it forces GNATprove to check that there is + -- room for one more element at the left of Index_Type. + + type Sequence is private + with Default_Initial_Condition => Length (Sequence) = 0, + Iterable => (First => Iter_First, + Has_Element => Iter_Has_Element, + Next => Iter_Next, + Element => Get); + -- Sequences are empty when default initialized. + -- Quantification over sequences can be done using the regular + -- quantification over its range or directky on its elements using for of. + + -- Sequences are axiomatized using Length and Get providing respectively + -- the length of a sequence and an accessor to its Nth element: + + function Length (S : Sequence) return Count_Type with + Global => null, + Post => (Index_Type'Pos (Index_Type'First) - 1) + Length'Result <= + Index_Type'Pos (Index_Type'Last); + + function Last (S : Sequence) return Extended_Index with + Global => null, + Post => Last'Result = + Index_Type'Val ((Index_Type'Pos (Index_Type'First) - 1) + Length (S)); + + function First return Extended_Index is (Index_Type'First); + + function Get (S : Sequence; N : Extended_Index) return Element_Type + -- Get ranges over Extended_Index so that it can be used for iteration. + + with + Global => null, + Pre => N in Index_Type'First .. Last (S); + + function "=" (S1, S2 : Sequence) return Boolean with + -- Extensional equality over sequences. + + Global => null, + Post => "="'Result = + (Length (S1) = Length (S2) + and then (for all N in Index_Type'First .. Last (S1) => + Get (S1, N) = Get (S2, N))); + + function "<" (S1, S2 : Sequence) return Boolean with + -- S1 is a strict subsequence of S2 + + Global => null, + Post => "<"'Result = + (Length (S1) < Length (S2) + and then (for all N in Index_Type'First .. Last (S1) => + Get (S1, N) = Get (S2, N))); + + function "<=" (S1, S2 : Sequence) return Boolean with + -- S1 is a subsequence of S2 + + Global => null, + Post => "<="'Result = + (Length (S1) <= Length (S2) + and then (for all N in Index_Type'First .. Last (S1) => + Get (S1, N) = Get (S2, N))); + + function Is_Set + (S : Sequence; N : Index_Type; E : Element_Type; Result : Sequence) + return Boolean + -- Returns True if Result is S where the Nth element has been replaced by + -- E. + + with + Global => null, + Post => Is_Set'Result = + (N in Index_Type'First .. Last (S) + and then Length (Result) = Length (S) + and then Get (Result, N) = E + and then (for all M in Index_Type'First .. Last (S) => + (if M /= N then Get (Result, M) = Get (S, M)))); + + function Set + (S : Sequence; N : Index_Type; E : Element_Type) return Sequence + -- Returns S where the Nth element has been replaced by E. + -- Is_Set (S, N, E, Result) should be instead of than + -- Result = Set (S, N, E) whenever possible both for execution and for + -- proof. + + with + Global => null, + Pre => N in Index_Type'First .. Last (S), + Post => Is_Set (S, N, E, Set'Result); + + function Is_Add + (S : Sequence; E : Element_Type; Result : Sequence) return Boolean + -- Returns True if Result is S appended with E. + + with + Global => null, + Post => Is_Add'Result = + (Length (Result) = Length (S) + 1 + and then Get (Result, Last (Result)) = E + and then (for all M in Index_Type'First .. Last (S) => + Get (Result, M) = Get (S, M))); + + function Add (S : Sequence; E : Element_Type) return Sequence with + -- Returns S appended with E. + -- Is_Add (S, E, Result) should be used instead of Result = Add (S, E) + -- whenever possible both for execution and for proof. + + Global => null, + Pre => Length (S) < Count_Type'Last and Last (S) < Index_Type'Last, + Post => Is_Add (S, E, Add'Result); + + --------------------------- + -- Iteration Primitives -- + --------------------------- + + function Iter_First (S : Sequence) return Extended_Index with + Global => null; + function Iter_Has_Element (S : Sequence; I : Extended_Index) return Boolean + with + Global => null, + Post => Iter_Has_Element'Result = (I in Index_Type'First .. Last (S)); + pragma Annotate (GNATprove, Inline_For_Proof, Iter_Has_Element); + + function Iter_Next (S : Sequence; I : Extended_Index) return Extended_Index + with + Global => null, + Pre => Iter_Has_Element (S, I); + +private + pragma SPARK_Mode (Off); + + package Containers is new Ada.Containers.Functional_Base + (Index_Type => Index_Type, + Element_Type => Element_Type); + + type Sequence is record + Content : Containers.Container; + end record; + + function Iter_First (S : + Sequence) return Extended_Index + is (Index_Type'First); + function Iter_Next (S : Sequence; I : Extended_Index) return Extended_Index + is + (if I = Extended_Index'Last then Extended_Index'First + else Extended_Index'Succ (I)); + + function Iter_Has_Element (S : Sequence; I : Extended_Index) return Boolean + is + (I in Index_Type'First .. + (Index_Type'Val + ((Index_Type'Pos (Index_Type'First) - 1) + Length (S)))); +end Ada.Containers.Functional_Vectors; diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb index 6f0dace3f9c..2833fff87a1 100644 --- a/gcc/ada/checks.adb +++ b/gcc/ada/checks.adb @@ -6697,20 +6697,9 @@ package body Checks is Set_Etype (N, Target_Base_Type); end Convert_And_Check_Range; - -- Local variables - - Checks_On : constant Boolean := - not Index_Checks_Suppressed (Target_Type) - or else - not Range_Checks_Suppressed (Target_Type); - -- Start of processing for Generate_Range_Check begin - if not Expander_Active or not Checks_On then - return; - end if; - -- First special case, if the source type is already within the range -- of the target type, then no check is needed (probably we should have -- stopped Do_Range_Check from being set in the first place, but better diff --git a/gcc/ada/cstand.adb b/gcc/ada/cstand.adb index 891fced9b19..5989530c9ff 100644 --- a/gcc/ada/cstand.adb +++ b/gcc/ada/cstand.adb @@ -1194,6 +1194,7 @@ package body CStand is Set_Etype (Any_Access, Any_Access); Init_Size (Any_Access, System_Address_Size); Set_Elem_Alignment (Any_Access); + Set_Directly_Designated_Type (Any_Access, Any_Type); Any_Character := New_Standard_Entity ("a character type"); Set_Ekind (Any_Character, E_Enumeration_Type); diff --git a/gcc/ada/impunit.adb b/gcc/ada/impunit.adb index e1cce657420..c53391a17bd 100644 --- a/gcc/ada/impunit.adb +++ b/gcc/ada/impunit.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 2000-2016, Free Software Foundation, Inc. -- +-- Copyright (C) 2000-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- -- @@ -590,6 +590,9 @@ package body Impunit is ("a-cfinve", F), -- Ada.Containers.Formal_Indefinite_Vectors ("a-coboho", F), -- Ada.Containers.Bounded_Holders ("a-cofove", F), -- Ada.Containers.Formal_Vectors + ("a-cofuma", F), -- Ada.Containers.Functional_Maps + ("a-cofuse", F), -- Ada.Containers.Functional_Sets + ("a-cofuve", F), -- Ada.Containers.Functional_Vectors ("a-cfdlli", F), -- Ada.Containers.Formal_Doubly_Linked_Lists ("a-cforse", F), -- Ada.Containers.Formal_Ordered_Sets ("a-cforma", F), -- Ada.Containers.Formal_Ordered_Maps diff --git a/gcc/ada/lib-xref.adb b/gcc/ada/lib-xref.adb index 4d9fe6919e4..bcb1b6cfcad 100644 --- a/gcc/ada/lib-xref.adb +++ b/gcc/ada/lib-xref.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1998-2016, Free Software Foundation, Inc. -- +-- Copyright (C) 1998-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- -- @@ -848,8 +848,8 @@ package body Lib.Xref is if Has_Unreferenced (E) and then In_Same_Extended_Unit (E, N) then - -- A reference as a named parameter in a call does not count - -- as a violation of pragma Unreferenced for this purpose... + -- A reference as a named parameter in a call does not count as a + -- violation of pragma Unreferenced for this purpose... if Nkind (N) = N_Identifier and then Nkind (Parent (N)) = N_Parameter_Association @@ -857,12 +857,22 @@ package body Lib.Xref is then null; - -- ... Neither does a reference to a variable on the left side - -- of an assignment. + -- ... Neither does a reference to a variable on the left side of + -- an assignment. elsif Is_On_LHS (N) then null; + -- Do not consider F'Result as a violation of pragma Unreferenced + -- since the attribute acts as an anonymous alias of the function + -- result and not as a real reference to the function. + + elsif Ekind_In (E, E_Function, E_Generic_Function) + and then Is_Entity_Name (N) + and then Is_Attribute_Result (Parent (N)) + then + null; + -- No warning if the reference is in a call that does not come -- from source (e.g. a call to a controlled type primitive). diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index 91f474279f5..790b6f6bcb9 100644 --- a/gcc/ada/sem_attr.adb +++ b/gcc/ada/sem_attr.adb @@ -6220,7 +6220,7 @@ package body Sem_Attr is -- single dereference link in a composite type. procedure Compute_Type_Key (T : Entity_Id); - -- Create a CRC integer from the declaration of the type, For a + -- Create a CRC integer from the declaration of the type. For a -- composite type, fold in the representation of its components in -- recursive fashion. We use directly the source representation of -- the types involved. @@ -6245,19 +6245,13 @@ package body Sem_Attr is ----------------------------- procedure Process_One_Declaration is - Ptr : Source_Ptr; - begin - Ptr := P_Min; - -- Scan type declaration, skipping blanks - while Ptr <= P_Max loop + for Ptr in P_Min .. P_Max loop if Buffer (Ptr) /= ' ' then System.CRC32.Update (CRC, Buffer (Ptr)); end if; - - Ptr := Ptr + 1; end loop; end Process_One_Declaration; @@ -6284,7 +6278,8 @@ package body Sem_Attr is end if; Sloc_Range (Enclosing_Declaration (T), P_Min, P_Max); - SFI := Get_Source_File_Index (P_Min); + SFI := Get_Source_File_Index (P_Min); + pragma Assert (SFI = Get_Source_File_Index (P_Max)); Buffer := Source_Text (SFI); Process_One_Declaration; @@ -6301,7 +6296,7 @@ package body Sem_Attr is end if; elsif Is_Derived_Type (T) then - Compute_Type_Key (Etype (T)); + Compute_Type_Key (Etype (T)); elsif Is_Record_Type (T) then declare @@ -6323,6 +6318,8 @@ package body Sem_Attr is while Present (Rep) loop if Comes_From_Source (Rep) then Sloc_Range (Rep, P_Min, P_Max); + pragma Assert (SFI = Get_Source_File_Index (P_Min)); + pragma Assert (SFI = Get_Source_File_Index (P_Max)); Process_One_Declaration; end if; diff --git a/gcc/ada/sem_type.adb b/gcc/ada/sem_type.adb index d14535a768a..1e5199dc403 100644 --- a/gcc/ada/sem_type.adb +++ b/gcc/ada/sem_type.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- -- @@ -802,8 +802,8 @@ package body Sem_Type is -- Start of processing for Covers begin - -- If either operand missing, then this is an error, but ignore it (and - -- pretend we have a cover) if errors already detected, since this may + -- If either operand is missing, then this is an error, but ignore it + -- and pretend we have a cover if errors already detected since this may -- simply mean we have malformed trees or a semantic error upstream. if No (T1) or else No (T2) then diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 05d906e8e53..de8dcedf5ba 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -3229,7 +3229,7 @@ package body Sem_Util is Result_Seen : in out Boolean) is procedure Check_Conjunct (Expr : Node_Id); - -- Check an individual conjunct in a conjunctions of Boolean + -- Check an individual conjunct in a conjunction of Boolean -- expressions, connected by "and" or "and then" operators. procedure Check_Conjuncts (Expr : Node_Id); @@ -3286,12 +3286,12 @@ package body Sem_Util is function Applied_On_Conjunct return Boolean is begin - -- Expr is the conjunct of an "and" enclosing expression + -- Expr is the conjunct of an enclosing "and" expression return Nkind (Parent (Expr)) in N_Subexpr - -- or Expr is a conjunct of an "and then" enclosing - -- expression in a postcondition aspect, which was split in + -- or Expr is a conjunct of an enclosing "and then" + -- expression in a postcondition aspect that was split into -- multiple pragmas. The first conjunct has the "and then" -- expression as Original_Node, and other conjuncts have -- Split_PCC set to True.