diff options
| author | Ian Lance Taylor <iant@golang.org> | 2021-10-27 08:47:25 -0700 |
|---|---|---|
| committer | Ian Lance Taylor <iant@golang.org> | 2021-10-27 08:47:25 -0700 |
| commit | a6d3012b274f38b20e2a57162106f625746af6c6 (patch) | |
| tree | 09ff8b13eb8ff7594c27dc8812efbf696dc97484 /gcc/ada/libgnat | |
| parent | cd2fd5facb5e1882d3f338ed456ae9536f7c0593 (diff) | |
| parent | 99b1021d21e5812ed01221d8fca8e8a32488a934 (diff) | |
| download | gcc-a6d3012b274f38b20e2a57162106f625746af6c6.zip gcc-a6d3012b274f38b20e2a57162106f625746af6c6.tar.gz gcc-a6d3012b274f38b20e2a57162106f625746af6c6.tar.bz2 | |
Merge from trunk revision 99b1021d21e5812ed01221d8fca8e8a32488a934.
Diffstat (limited to 'gcc/ada/libgnat')
35 files changed, 524 insertions, 1624 deletions
diff --git a/gcc/ada/libgnat/a-calend.adb b/gcc/ada/libgnat/a-calend.adb index 5dedfc5..b24e95d 100644 --- a/gcc/ada/libgnat/a-calend.adb +++ b/gcc/ada/libgnat/a-calend.adb @@ -149,7 +149,7 @@ is -- Leap seconds control -- -------------------------- - Flag : Integer; + Flag : constant Integer; pragma Import (C, Flag, "__gl_leap_seconds_support"); -- This imported value is used to determine whether the compilation had -- binder flag "-y" present which enables leap seconds. A value of zero diff --git a/gcc/ada/libgnat/a-excach.adb b/gcc/ada/libgnat/a-excach.adb index 3939287..a8e6a58 100644 --- a/gcc/ada/libgnat/a-excach.adb +++ b/gcc/ada/libgnat/a-excach.adb @@ -41,7 +41,7 @@ pragma Warnings (On); separate (Ada.Exceptions) procedure Call_Chain (Excep : EOA) is - Exception_Tracebacks : Integer; + Exception_Tracebacks : constant Integer; pragma Import (C, Exception_Tracebacks, "__gl_exception_tracebacks"); -- Boolean indicating whether tracebacks should be stored in exception -- occurrences. diff --git a/gcc/ada/libgnat/a-except.adb b/gcc/ada/libgnat/a-except.adb index 5933928..631c35a 100644 --- a/gcc/ada/libgnat/a-except.adb +++ b/gcc/ada/libgnat/a-except.adb @@ -1760,7 +1760,7 @@ package body Ada.Exceptions is -- Wide_Exception_Name -- ------------------------- - WC_Encoding : Character; + WC_Encoding : constant Character; pragma Import (C, WC_Encoding, "__gl_wc_encoding"); -- Encoding method for source, as exported by binder diff --git a/gcc/ada/libgnat/g-io-put__vxworks.adb b/gcc/ada/libgnat/a-nbnbin__ghost.adb index 29307f9..7d22086 100644 --- a/gcc/ada/libgnat/g-io-put__vxworks.adb +++ b/gcc/ada/libgnat/a-nbnbin__ghost.adb @@ -2,11 +2,11 @@ -- -- -- GNAT RUN-TIME COMPONENTS -- -- -- --- G N A T . I O -- +-- ADA.NUMERICS.BIG_NUMBERS.BIG_INTEGERS -- -- -- -- B o d y -- -- -- --- Copyright (C) 1995-2021, AdaCore -- +-- Copyright (C) 2021, 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- -- @@ -29,25 +29,48 @@ -- -- ------------------------------------------------------------------------------ --- vxworks zfp version of Put (C : Character) +-- This body is provided as a work-around for a GNAT compiler bug, as GNAT +-- currently does not compile instantiations of the spec with imported ghost +-- generics for packages Signed_Conversions and Unsigned_Conversions. -with Interfaces.C; use Interfaces.C; +package body Ada.Numerics.Big_Numbers.Big_Integers with + SPARK_Mode => Off +is -separate (GNAT.IO) -procedure Put (C : Character) is + package body Signed_Conversions with + SPARK_Mode => Off + is - function ioGlobalStdGet - (File : int) return int; - pragma Import (C, ioGlobalStdGet, "ioGlobalStdGet"); + function To_Big_Integer (Arg : Int) return Valid_Big_Integer is + begin + raise Program_Error; + return (null record); + end To_Big_Integer; - procedure fdprintf - (File : int; - Format : String; - Value : Character); - pragma Import (C, fdprintf, "fdprintf"); + function From_Big_Integer (Arg : Valid_Big_Integer) return Int is + begin + raise Program_Error; + return 0; + end From_Big_Integer; - Stdout_ID : constant int := 1; + end Signed_Conversions; -begin - fdprintf (ioGlobalStdGet (Stdout_ID), "%c" & ASCII.NUL, C); -end Put; + package body Unsigned_Conversions with + SPARK_Mode => Off + is + + function To_Big_Integer (Arg : Int) return Valid_Big_Integer is + begin + raise Program_Error; + return (null record); + end To_Big_Integer; + + function From_Big_Integer (Arg : Valid_Big_Integer) return Int is + begin + raise Program_Error; + return 0; + end From_Big_Integer; + + end Unsigned_Conversions; + +end Ada.Numerics.Big_Numbers.Big_Integers; diff --git a/gcc/ada/libgnat/a-nbnbin__ghost.ads b/gcc/ada/libgnat/a-nbnbin__ghost.ads new file mode 100644 index 0000000..3663dd7 --- /dev/null +++ b/gcc/ada/libgnat/a-nbnbin__ghost.ads @@ -0,0 +1,202 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT RUN-TIME COMPONENTS -- +-- -- +-- ADA.NUMERICS.BIG_NUMBERS.BIG_INTEGERS -- +-- -- +-- S p e c -- +-- -- +-- This specification is derived from the Ada Reference Manual for use with -- +-- GNAT. In accordance with the copyright of that document, you can freely -- +-- copy and modify this specification, provided that if you redistribute a -- +-- modified version, any changes that you have made are clearly indicated. -- +-- -- +------------------------------------------------------------------------------ + +package Ada.Numerics.Big_Numbers.Big_Integers with + SPARK_Mode, + Ghost, + Preelaborate +is + type Big_Integer is private + with Integer_Literal => From_Universal_Image; + + function Is_Valid (Arg : Big_Integer) return Boolean + with + Import, + Global => null; + + subtype Valid_Big_Integer is Big_Integer + with Dynamic_Predicate => Is_Valid (Valid_Big_Integer), + Predicate_Failure => raise Program_Error; + + function "=" (L, R : Valid_Big_Integer) return Boolean with + Import, + Global => null; + + function "<" (L, R : Valid_Big_Integer) return Boolean with + Import, + Global => null; + + function "<=" (L, R : Valid_Big_Integer) return Boolean with + Import, + Global => null; + + function ">" (L, R : Valid_Big_Integer) return Boolean with + Import, + Global => null; + + function ">=" (L, R : Valid_Big_Integer) return Boolean with + Import, + Global => null; + + function To_Big_Integer (Arg : Integer) return Valid_Big_Integer + with + Import, + Global => null; + + subtype Big_Positive is Big_Integer + with Dynamic_Predicate => + (if Is_Valid (Big_Positive) + then Big_Positive > To_Big_Integer (0)), + Predicate_Failure => (raise Constraint_Error); + + subtype Big_Natural is Big_Integer + with Dynamic_Predicate => + (if Is_Valid (Big_Natural) + then Big_Natural >= To_Big_Integer (0)), + Predicate_Failure => (raise Constraint_Error); + + function In_Range + (Arg : Valid_Big_Integer; Low, High : Big_Integer) return Boolean + is (Low <= Arg and Arg <= High) + with + Import, + Global => null; + + function To_Integer (Arg : Valid_Big_Integer) return Integer + with + Import, + Pre => In_Range (Arg, + Low => To_Big_Integer (Integer'First), + High => To_Big_Integer (Integer'Last)) + or else (raise Constraint_Error), + Global => null; + + generic + type Int is range <>; + package Signed_Conversions is + + function To_Big_Integer (Arg : Int) return Valid_Big_Integer + with + Global => null; + + function From_Big_Integer (Arg : Valid_Big_Integer) return Int + with + Pre => In_Range (Arg, + Low => To_Big_Integer (Int'First), + High => To_Big_Integer (Int'Last)) + or else (raise Constraint_Error), + Global => null; + end Signed_Conversions; + + generic + type Int is mod <>; + package Unsigned_Conversions is + + function To_Big_Integer (Arg : Int) return Valid_Big_Integer + with + Global => null; + + function From_Big_Integer (Arg : Valid_Big_Integer) return Int + with + Pre => In_Range (Arg, + Low => To_Big_Integer (Int'First), + High => To_Big_Integer (Int'Last)) + or else (raise Constraint_Error), + Global => null; + + end Unsigned_Conversions; + + function From_String (Arg : String) return Valid_Big_Integer + with + Import, + Global => null; + + function From_Universal_Image (Arg : String) return Valid_Big_Integer + renames From_String; + + function "+" (L : Valid_Big_Integer) return Valid_Big_Integer + with + Import, + Global => null; + + function "-" (L : Valid_Big_Integer) return Valid_Big_Integer + with + Import, + Global => null; + + function "abs" (L : Valid_Big_Integer) return Valid_Big_Integer + with + Import, + Global => null; + + function "+" (L, R : Valid_Big_Integer) return Valid_Big_Integer + with + Import, + Global => null; + + function "-" (L, R : Valid_Big_Integer) return Valid_Big_Integer + with + Import, + Global => null; + + function "*" (L, R : Valid_Big_Integer) return Valid_Big_Integer + with + Import, + Global => null; + + function "/" (L, R : Valid_Big_Integer) return Valid_Big_Integer + with + Import, + Global => null; + + function "mod" (L, R : Valid_Big_Integer) return Valid_Big_Integer + with + Import, + Global => null; + + function "rem" (L, R : Valid_Big_Integer) return Valid_Big_Integer + with + Import, + Global => null; + + function "**" (L : Valid_Big_Integer; R : Natural) return Valid_Big_Integer + with + Import, + Global => null; + + function Min (L, R : Valid_Big_Integer) return Valid_Big_Integer + with + Import, + Global => null; + + function Max (L, R : Valid_Big_Integer) return Valid_Big_Integer + with + Import, + Global => null; + + function Greatest_Common_Divisor + (L, R : Valid_Big_Integer) return Big_Positive + with + Import, + Pre => (L /= To_Big_Integer (0) and R /= To_Big_Integer (0)) + or else (raise Constraint_Error), + Global => null; + +private + pragma SPARK_Mode (Off); + + type Big_Integer is null record; + +end Ada.Numerics.Big_Numbers.Big_Integers; diff --git a/gcc/ada/libgnat/a-nbnbin__gmp.adb b/gcc/ada/libgnat/a-nbnbin__gmp.adb index 880e9a3..1516f49 100644 --- a/gcc/ada/libgnat/a-nbnbin__gmp.adb +++ b/gcc/ada/libgnat/a-nbnbin__gmp.adb @@ -327,7 +327,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is -- From_String -- ----------------- - function From_String (Arg : String) return Big_Integer is + function From_String (Arg : String) return Valid_Big_Integer is function mpz_set_str (this : access mpz_t; str : System.Address; diff --git a/gcc/ada/libgnat/a-strsup.ads b/gcc/ada/libgnat/a-strsup.ads index 7428e9c..ae4339f 100644 --- a/gcc/ada/libgnat/a-strsup.ads +++ b/gcc/ada/libgnat/a-strsup.ads @@ -76,7 +76,8 @@ package Ada.Strings.Superbounded with SPARK_Mode is -- that they can be renamed in Ada.Strings.Bounded.Generic_Bounded_Length. function Super_Length (Source : Super_String) return Natural - is (Source.Current_Length); + is (Source.Current_Length) + with Global => null; -------------------------------------------------------- -- Conversion, Concatenation, and Selection Functions -- @@ -620,7 +621,8 @@ package Ada.Strings.Superbounded with SPARK_Mode is is (if Index <= Source.Current_Length then Source.Data (Index) else raise Index_Error) - with Pre => Index <= Super_Length (Source); + with Pre => Index <= Super_Length (Source), + Global => null; procedure Super_Replace_Element (Source : in out Super_String; @@ -649,8 +651,9 @@ package Ada.Strings.Superbounded with SPARK_Mode is -- get the null string in accordance with normal Ada slice rules. String (Source.Data (Low .. High))) - with Pre => Low - 1 <= Super_Length (Source) - and then High <= Super_Length (Source); + with Pre => Low - 1 <= Super_Length (Source) + and then High <= Super_Length (Source), + Global => null; function Super_Slice (Source : Super_String; diff --git a/gcc/ada/libgnat/a-strunb.adb b/gcc/ada/libgnat/a-strunb.adb index 4727f965..0d62e4b 100644 --- a/gcc/ada/libgnat/a-strunb.adb +++ b/gcc/ada/libgnat/a-strunb.adb @@ -505,8 +505,14 @@ package body Ada.Strings.Unbounded is -- Note: Don't try to free statically allocated null string if Object.Reference /= Null_String'Access then - Deallocate (Object.Reference); - Object.Reference := Null_Unbounded_String.Reference; + declare + Reference_Copy : String_Access := Object.Reference; + -- The original reference cannot be null, so we must create a + -- copy which will become null when deallocated. + begin + Deallocate (Reference_Copy); + Object.Reference := Null_Unbounded_String.Reference; + end; Object.Last := 0; end if; end Finalize; diff --git a/gcc/ada/libgnat/a-strunb.ads b/gcc/ada/libgnat/a-strunb.ads index b3050fd..2f5bd94 100644 --- a/gcc/ada/libgnat/a-strunb.ads +++ b/gcc/ada/libgnat/a-strunb.ads @@ -746,8 +746,8 @@ private renames To_Unbounded_String; type Unbounded_String is new AF.Controlled with record - Reference : String_Access := Null_String'Access; - Last : Natural := 0; + Reference : not null String_Access := Null_String'Access; + Last : Natural := 0; end record with Put_Image => Put_Image; procedure Put_Image diff --git a/gcc/ada/libgnat/a-tags.adb b/gcc/ada/libgnat/a-tags.adb index c6a9d25..170d16a 100644 --- a/gcc/ada/libgnat/a-tags.adb +++ b/gcc/ada/libgnat/a-tags.adb @@ -1032,7 +1032,7 @@ package body Ada.Tags is -- Wide_Expanded_Name -- ------------------------ - WC_Encoding : Character; + WC_Encoding : constant Character; pragma Import (C, WC_Encoding, "__gl_wc_encoding"); -- Encoding method for source, as exported by binder diff --git a/gcc/ada/libgnat/a-textio.adb b/gcc/ada/libgnat/a-textio.adb index 8667360..1bdab6e 100644 --- a/gcc/ada/libgnat/a-textio.adb +++ b/gcc/ada/libgnat/a-textio.adb @@ -67,7 +67,7 @@ is use type System.CRTL.size_t; - WC_Encoding : Character; + WC_Encoding : constant Character; pragma Import (C, WC_Encoding, "__gl_wc_encoding"); -- Default wide character encoding diff --git a/gcc/ada/libgnat/a-witeio.adb b/gcc/ada/libgnat/a-witeio.adb index 7dbd3b3..dbc0f2a 100644 --- a/gcc/ada/libgnat/a-witeio.adb +++ b/gcc/ada/libgnat/a-witeio.adb @@ -55,7 +55,7 @@ package body Ada.Wide_Text_IO is use type System.CRTL.size_t; - WC_Encoding : Character; + WC_Encoding : constant Character; pragma Import (C, WC_Encoding, "__gl_wc_encoding"); -- Default wide character encoding diff --git a/gcc/ada/libgnat/a-ztexio.adb b/gcc/ada/libgnat/a-ztexio.adb index 71d733e..b72a1d4 100644 --- a/gcc/ada/libgnat/a-ztexio.adb +++ b/gcc/ada/libgnat/a-ztexio.adb @@ -55,7 +55,7 @@ package body Ada.Wide_Wide_Text_IO is use type System.CRTL.size_t; - WC_Encoding : Character; + WC_Encoding : constant Character; pragma Import (C, WC_Encoding, "__gl_wc_encoding"); -- Default wide character encoding diff --git a/gcc/ada/libgnat/g-binenv.adb b/gcc/ada/libgnat/g-binenv.adb index e10fb96..4bf39cd 100644 --- a/gcc/ada/libgnat/g-binenv.adb +++ b/gcc/ada/libgnat/g-binenv.adb @@ -40,7 +40,7 @@ package body GNAT.Bind_Environment is function Get (Key : String) return String is use type System.Address; - Bind_Env_Addr : System.Address; + Bind_Env_Addr : constant System.Address; pragma Import (C, Bind_Env_Addr, "__gl_bind_env_addr"); -- Variable provided by init.c/s-init.ads, and initialized by -- the binder generated file. diff --git a/gcc/ada/libgnat/s-aoinar.adb b/gcc/ada/libgnat/s-aoinar.adb index 2f430ed..41d0cda 100644 --- a/gcc/ada/libgnat/s-aoinar.adb +++ b/gcc/ada/libgnat/s-aoinar.adb @@ -72,22 +72,10 @@ package body System.Atomic_Operations.Integer_Arithmetic is Value : Atomic_Type) return Atomic_Type is pragma Warnings (Off); - function Atomic_Fetch_Add_1 + function Atomic_Fetch_Add (Ptr : System.Address; Val : Atomic_Type; Model : Mem_Model := Seq_Cst) return Atomic_Type; - pragma Import (Intrinsic, Atomic_Fetch_Add_1, "__atomic_fetch_add_1"); - function Atomic_Fetch_Add_2 - (Ptr : System.Address; Val : Atomic_Type; Model : Mem_Model := Seq_Cst) - return Atomic_Type; - pragma Import (Intrinsic, Atomic_Fetch_Add_2, "__atomic_fetch_add_2"); - function Atomic_Fetch_Add_4 - (Ptr : System.Address; Val : Atomic_Type; Model : Mem_Model := Seq_Cst) - return Atomic_Type; - pragma Import (Intrinsic, Atomic_Fetch_Add_4, "__atomic_fetch_add_4"); - function Atomic_Fetch_Add_8 - (Ptr : System.Address; Val : Atomic_Type; Model : Mem_Model := Seq_Cst) - return Atomic_Type; - pragma Import (Intrinsic, Atomic_Fetch_Add_8, "__atomic_fetch_add_8"); + pragma Import (Intrinsic, Atomic_Fetch_Add, "__atomic_fetch_add"); pragma Warnings (On); begin @@ -96,21 +84,14 @@ package body System.Atomic_Operations.Integer_Arithmetic is if Atomic_Type'Base'Last = Atomic_Type'Last and then Atomic_Type'Base'First = Atomic_Type'First - and then Atomic_Type'Last - in 2 ** 7 - 1 | 2 ** 15 - 1 | 2 ** 31 - 1 | 2 ** 63 - 1 + and then Atomic_Type'Last = 2**(Atomic_Type'Object_Size - 1) - 1 then - case Long_Long_Integer (Atomic_Type'Last) is - when 2 ** 7 - 1 => - return Atomic_Fetch_Add_1 (Item'Address, Value); - when 2 ** 15 - 1 => - return Atomic_Fetch_Add_2 (Item'Address, Value); - when 2 ** 31 - 1 => - return Atomic_Fetch_Add_4 (Item'Address, Value); - when 2 ** 63 - 1 => - return Atomic_Fetch_Add_8 (Item'Address, Value); - when others => - raise Program_Error; - end case; + if Atomic_Type'Object_Size in 8 | 16 | 32 | 64 then + return Atomic_Fetch_Add (Item'Address, Value); + else + raise Program_Error; + end if; + else declare Old_Value : aliased Atomic_Type := Item; @@ -138,22 +119,10 @@ package body System.Atomic_Operations.Integer_Arithmetic is Value : Atomic_Type) return Atomic_Type is pragma Warnings (Off); - function Atomic_Fetch_Sub_1 + function Atomic_Fetch_Sub (Ptr : System.Address; Val : Atomic_Type; Model : Mem_Model := Seq_Cst) return Atomic_Type; - pragma Import (Intrinsic, Atomic_Fetch_Sub_1, "__atomic_fetch_sub_1"); - function Atomic_Fetch_Sub_2 - (Ptr : System.Address; Val : Atomic_Type; Model : Mem_Model := Seq_Cst) - return Atomic_Type; - pragma Import (Intrinsic, Atomic_Fetch_Sub_2, "__atomic_fetch_sub_2"); - function Atomic_Fetch_Sub_4 - (Ptr : System.Address; Val : Atomic_Type; Model : Mem_Model := Seq_Cst) - return Atomic_Type; - pragma Import (Intrinsic, Atomic_Fetch_Sub_4, "__atomic_fetch_sub_4"); - function Atomic_Fetch_Sub_8 - (Ptr : System.Address; Val : Atomic_Type; Model : Mem_Model := Seq_Cst) - return Atomic_Type; - pragma Import (Intrinsic, Atomic_Fetch_Sub_8, "__atomic_fetch_sub_8"); + pragma Import (Intrinsic, Atomic_Fetch_Sub, "__atomic_fetch_sub"); pragma Warnings (On); begin @@ -162,21 +131,14 @@ package body System.Atomic_Operations.Integer_Arithmetic is if Atomic_Type'Base'Last = Atomic_Type'Last and then Atomic_Type'Base'First = Atomic_Type'First - and then Atomic_Type'Last - in 2 ** 7 - 1 | 2 ** 15 - 1 | 2 ** 31 - 1 | 2 ** 63 - 1 + and then Atomic_Type'Last = 2**(Atomic_Type'Object_Size - 1) - 1 then - case Long_Long_Integer (Atomic_Type'Last) is - when 2 ** 7 - 1 => - return Atomic_Fetch_Sub_1 (Item'Address, Value); - when 2 ** 15 - 1 => - return Atomic_Fetch_Sub_2 (Item'Address, Value); - when 2 ** 31 - 1 => - return Atomic_Fetch_Sub_4 (Item'Address, Value); - when 2 ** 63 - 1 => - return Atomic_Fetch_Sub_8 (Item'Address, Value); - when others => - raise Program_Error; - end case; + if Atomic_Type'Object_Size in 8 | 16 | 32 | 64 then + return Atomic_Fetch_Sub (Item'Address, Value); + else + raise Program_Error; + end if; + else declare Old_Value : aliased Atomic_Type := Item; diff --git a/gcc/ada/libgnat/s-aomoar.adb b/gcc/ada/libgnat/s-aomoar.adb index a6f4b0e..617a5b3 100644 --- a/gcc/ada/libgnat/s-aomoar.adb +++ b/gcc/ada/libgnat/s-aomoar.adb @@ -72,48 +72,26 @@ package body System.Atomic_Operations.Modular_Arithmetic is Value : Atomic_Type) return Atomic_Type is pragma Warnings (Off); - function Atomic_Fetch_Add_1 + function Atomic_Fetch_Add (Ptr : System.Address; Val : Atomic_Type; Model : Mem_Model := Seq_Cst) return Atomic_Type; - pragma Import (Intrinsic, Atomic_Fetch_Add_1, "__atomic_fetch_add_1"); - function Atomic_Fetch_Add_2 - (Ptr : System.Address; Val : Atomic_Type; Model : Mem_Model := Seq_Cst) - return Atomic_Type; - pragma Import (Intrinsic, Atomic_Fetch_Add_2, "__atomic_fetch_add_2"); - function Atomic_Fetch_Add_4 - (Ptr : System.Address; Val : Atomic_Type; Model : Mem_Model := Seq_Cst) - return Atomic_Type; - pragma Import (Intrinsic, Atomic_Fetch_Add_4, "__atomic_fetch_add_4"); - function Atomic_Fetch_Add_8 - (Ptr : System.Address; Val : Atomic_Type; Model : Mem_Model := Seq_Cst) - return Atomic_Type; - pragma Import (Intrinsic, Atomic_Fetch_Add_8, "__atomic_fetch_add_8"); + pragma Import (Intrinsic, Atomic_Fetch_Add, "__atomic_fetch_add"); pragma Warnings (On); begin -- Use the direct intrinsics when possible, and fallback to -- compare-and-exchange otherwise. - -- Also suppress spurious warnings. - pragma Warnings (Off); if Atomic_Type'Base'Last = Atomic_Type'Last and then Atomic_Type'First = 0 - and then Atomic_Type'Last - in 2 ** 8 - 1 | 2 ** 16 - 1 | 2 ** 32 - 1 | 2 ** 64 - 1 + and then Atomic_Type'Last = 2**Atomic_Type'Object_Size - 1 then - pragma Warnings (On); - case Unsigned_64 (Atomic_Type'Last) is - when 2 ** 8 - 1 => - return Atomic_Fetch_Add_1 (Item'Address, Value); - when 2 ** 16 - 1 => - return Atomic_Fetch_Add_2 (Item'Address, Value); - when 2 ** 32 - 1 => - return Atomic_Fetch_Add_4 (Item'Address, Value); - when 2 ** 64 - 1 => - return Atomic_Fetch_Add_8 (Item'Address, Value); - when others => - raise Program_Error; - end case; + if Atomic_Type'Object_Size in 8 | 16 | 32 | 64 then + return Atomic_Fetch_Add (Item'Address, Value); + else + raise Program_Error; + end if; + else declare Old_Value : aliased Atomic_Type := Item; @@ -141,48 +119,26 @@ package body System.Atomic_Operations.Modular_Arithmetic is Value : Atomic_Type) return Atomic_Type is pragma Warnings (Off); - function Atomic_Fetch_Sub_1 + function Atomic_Fetch_Sub (Ptr : System.Address; Val : Atomic_Type; Model : Mem_Model := Seq_Cst) return Atomic_Type; - pragma Import (Intrinsic, Atomic_Fetch_Sub_1, "__atomic_fetch_sub_1"); - function Atomic_Fetch_Sub_2 - (Ptr : System.Address; Val : Atomic_Type; Model : Mem_Model := Seq_Cst) - return Atomic_Type; - pragma Import (Intrinsic, Atomic_Fetch_Sub_2, "__atomic_fetch_sub_2"); - function Atomic_Fetch_Sub_4 - (Ptr : System.Address; Val : Atomic_Type; Model : Mem_Model := Seq_Cst) - return Atomic_Type; - pragma Import (Intrinsic, Atomic_Fetch_Sub_4, "__atomic_fetch_sub_4"); - function Atomic_Fetch_Sub_8 - (Ptr : System.Address; Val : Atomic_Type; Model : Mem_Model := Seq_Cst) - return Atomic_Type; - pragma Import (Intrinsic, Atomic_Fetch_Sub_8, "__atomic_fetch_sub_8"); + pragma Import (Intrinsic, Atomic_Fetch_Sub, "__atomic_fetch_sub"); pragma Warnings (On); begin -- Use the direct intrinsics when possible, and fallback to -- compare-and-exchange otherwise. - -- Also suppress spurious warnings. - pragma Warnings (Off); if Atomic_Type'Base'Last = Atomic_Type'Last and then Atomic_Type'First = 0 - and then Atomic_Type'Last - in 2 ** 8 - 1 | 2 ** 16 - 1 | 2 ** 32 - 1 | 2 ** 64 - 1 + and then Atomic_Type'Last = 2**Atomic_Type'Object_Size - 1 then - pragma Warnings (On); - case Unsigned_64 (Atomic_Type'Last) is - when 2 ** 8 - 1 => - return Atomic_Fetch_Sub_1 (Item'Address, Value); - when 2 ** 16 - 1 => - return Atomic_Fetch_Sub_2 (Item'Address, Value); - when 2 ** 32 - 1 => - return Atomic_Fetch_Sub_4 (Item'Address, Value); - when 2 ** 64 - 1 => - return Atomic_Fetch_Sub_8 (Item'Address, Value); - when others => - raise Program_Error; - end case; + if Atomic_Type'Object_Size in 8 | 16 | 32 | 64 then + return Atomic_Fetch_Sub (Item'Address, Value); + else + raise Program_Error; + end if; + else declare Old_Value : aliased Atomic_Type := Item; diff --git a/gcc/ada/libgnat/s-atopex.adb b/gcc/ada/libgnat/s-atopex.adb index b0aa9e5..65e9433 100644 --- a/gcc/ada/libgnat/s-atopex.adb +++ b/gcc/ada/libgnat/s-atopex.adb @@ -43,36 +43,19 @@ package body System.Atomic_Operations.Exchange is Value : Atomic_Type) return Atomic_Type is pragma Warnings (Off); - function Atomic_Exchange_1 + function Atomic_Exchange (Ptr : System.Address; Val : Atomic_Type; Model : Mem_Model := Seq_Cst) return Atomic_Type; - pragma Import (Intrinsic, Atomic_Exchange_1, "__atomic_exchange_1"); - function Atomic_Exchange_2 - (Ptr : System.Address; - Val : Atomic_Type; - Model : Mem_Model := Seq_Cst) return Atomic_Type; - pragma Import (Intrinsic, Atomic_Exchange_2, "__atomic_exchange_2"); - function Atomic_Exchange_4 - (Ptr : System.Address; - Val : Atomic_Type; - Model : Mem_Model := Seq_Cst) return Atomic_Type; - pragma Import (Intrinsic, Atomic_Exchange_4, "__atomic_exchange_4"); - function Atomic_Exchange_8 - (Ptr : System.Address; - Val : Atomic_Type; - Model : Mem_Model := Seq_Cst) return Atomic_Type; - pragma Import (Intrinsic, Atomic_Exchange_8, "__atomic_exchange_8"); + pragma Import (Intrinsic, Atomic_Exchange, "__atomic_exchange_n"); pragma Warnings (On); begin - case Atomic_Type'Object_Size is - when 8 => return Atomic_Exchange_1 (Item'Address, Value); - when 16 => return Atomic_Exchange_2 (Item'Address, Value); - when 32 => return Atomic_Exchange_4 (Item'Address, Value); - when 64 => return Atomic_Exchange_8 (Item'Address, Value); - when others => raise Program_Error; - end case; + if Atomic_Type'Object_Size in 8 | 16 | 32 | 64 then + return Atomic_Exchange (Item'Address, Value); + else + raise Program_Error; + end if; end Atomic_Exchange; --------------------------------- @@ -85,34 +68,7 @@ package body System.Atomic_Operations.Exchange is Desired : Atomic_Type) return Boolean is pragma Warnings (Off); - function Atomic_Compare_Exchange_1 - (Ptr : System.Address; - Expected : System.Address; - Desired : Atomic_Type; - Weak : Boolean := False; - Success_Model : Mem_Model := Seq_Cst; - Failure_Model : Mem_Model := Seq_Cst) return Boolean; - pragma Import - (Intrinsic, Atomic_Compare_Exchange_1, "__atomic_compare_exchange_1"); - function Atomic_Compare_Exchange_2 - (Ptr : System.Address; - Expected : System.Address; - Desired : Atomic_Type; - Weak : Boolean := False; - Success_Model : Mem_Model := Seq_Cst; - Failure_Model : Mem_Model := Seq_Cst) return Boolean; - pragma Import - (Intrinsic, Atomic_Compare_Exchange_2, "__atomic_compare_exchange_2"); - function Atomic_Compare_Exchange_4 - (Ptr : System.Address; - Expected : System.Address; - Desired : Atomic_Type; - Weak : Boolean := False; - Success_Model : Mem_Model := Seq_Cst; - Failure_Model : Mem_Model := Seq_Cst) return Boolean; - pragma Import - (Intrinsic, Atomic_Compare_Exchange_4, "__atomic_compare_exchange_4"); - function Atomic_Compare_Exchange_8 + function Atomic_Compare_Exchange (Ptr : System.Address; Expected : System.Address; Desired : Atomic_Type; @@ -120,26 +76,15 @@ package body System.Atomic_Operations.Exchange is Success_Model : Mem_Model := Seq_Cst; Failure_Model : Mem_Model := Seq_Cst) return Boolean; pragma Import - (Intrinsic, Atomic_Compare_Exchange_8, "__atomic_compare_exchange_8"); + (Intrinsic, Atomic_Compare_Exchange, "__atomic_compare_exchange_n"); pragma Warnings (On); begin - case Atomic_Type'Object_Size is - when 8 => - return - Atomic_Compare_Exchange_1 (Item'Address, Prior'Address, Desired); - when 16 => - return - Atomic_Compare_Exchange_2 (Item'Address, Prior'Address, Desired); - when 32 => - return - Atomic_Compare_Exchange_4 (Item'Address, Prior'Address, Desired); - when 64 => - return - Atomic_Compare_Exchange_8 (Item'Address, Prior'Address, Desired); - when others => - raise Program_Error; - end case; + if Atomic_Type'Object_Size in 8 | 16 | 32 | 64 then + return Atomic_Compare_Exchange (Item'Address, Prior'Address, Desired); + else + raise Program_Error; + end if; end Atomic_Compare_And_Exchange; ------------------ diff --git a/gcc/ada/libgnat/s-atopri.adb b/gcc/ada/libgnat/s-atopri.adb index ba284f0..20aa666 100644 --- a/gcc/ada/libgnat/s-atopri.adb +++ b/gcc/ada/libgnat/s-atopri.adb @@ -31,103 +31,39 @@ package body System.Atomic_Primitives is - ---------------------- - -- Lock_Free_Read_8 -- - ---------------------- + -------------------- + -- Lock_Free_Read -- + -------------------- - function Lock_Free_Read_8 (Ptr : Address) return uint8 is - begin - if uint8'Atomic_Always_Lock_Free then - return Atomic_Load_8 (Ptr, Acquire); - else - raise Program_Error; - end if; - end Lock_Free_Read_8; - - ----------------------- - -- Lock_Free_Read_16 -- - ----------------------- + function Lock_Free_Read (Ptr : Address) return Atomic_Type is + function My_Atomic_Load is new Atomic_Load (Atomic_Type); - function Lock_Free_Read_16 (Ptr : Address) return uint16 is begin - if uint16'Atomic_Always_Lock_Free then - return Atomic_Load_16 (Ptr, Acquire); + if Atomic_Type'Atomic_Always_Lock_Free then + return My_Atomic_Load (Ptr, Acquire); else raise Program_Error; end if; - end Lock_Free_Read_16; + end Lock_Free_Read; - ----------------------- - -- Lock_Free_Read_32 -- - ----------------------- - - function Lock_Free_Read_32 (Ptr : Address) return uint32 is - begin - if uint32'Atomic_Always_Lock_Free then - return Atomic_Load_32 (Ptr, Acquire); - else - raise Program_Error; - end if; - end Lock_Free_Read_32; + ------------------------- + -- Lock_Free_Try_Write -- + ------------------------- - ----------------------- - -- Lock_Free_Read_64 -- - ----------------------- - - function Lock_Free_Read_64 (Ptr : Address) return uint64 is - begin - if uint64'Atomic_Always_Lock_Free then - return Atomic_Load_64 (Ptr, Acquire); - else - raise Program_Error; - end if; - end Lock_Free_Read_64; - - --------------------------- - -- Lock_Free_Try_Write_8 -- - --------------------------- - - function Lock_Free_Try_Write_8 + function Lock_Free_Try_Write (Ptr : Address; - Expected : in out uint8; - Desired : uint8) return Boolean + Expected : in out Atomic_Type; + Desired : Atomic_Type) return Boolean is - Actual : uint8; + function My_Sync_Compare_And_Swap is + new Sync_Compare_And_Swap (Atomic_Type); - begin - if Expected /= Desired then - - if uint8'Atomic_Always_Lock_Free then - Actual := Sync_Compare_And_Swap_8 (Ptr, Expected, Desired); - else - raise Program_Error; - end if; - - if Actual /= Expected then - Expected := Actual; - return False; - end if; - end if; - - return True; - end Lock_Free_Try_Write_8; - - ---------------------------- - -- Lock_Free_Try_Write_16 -- - ---------------------------- - - function Lock_Free_Try_Write_16 - (Ptr : Address; - Expected : in out uint16; - Desired : uint16) return Boolean - is - Actual : uint16; + Actual : Atomic_Type; begin if Expected /= Desired then - - if uint16'Atomic_Always_Lock_Free then - Actual := Sync_Compare_And_Swap_16 (Ptr, Expected, Desired); + if Atomic_Type'Atomic_Always_Lock_Free then + Actual := My_Sync_Compare_And_Swap (Ptr, Expected, Desired); else raise Program_Error; end if; @@ -139,63 +75,6 @@ package body System.Atomic_Primitives is end if; return True; - end Lock_Free_Try_Write_16; - - ---------------------------- - -- Lock_Free_Try_Write_32 -- - ---------------------------- + end Lock_Free_Try_Write; - function Lock_Free_Try_Write_32 - (Ptr : Address; - Expected : in out uint32; - Desired : uint32) return Boolean - is - Actual : uint32; - - begin - if Expected /= Desired then - - if uint32'Atomic_Always_Lock_Free then - Actual := Sync_Compare_And_Swap_32 (Ptr, Expected, Desired); - else - raise Program_Error; - end if; - - if Actual /= Expected then - Expected := Actual; - return False; - end if; - end if; - - return True; - end Lock_Free_Try_Write_32; - - ---------------------------- - -- Lock_Free_Try_Write_64 -- - ---------------------------- - - function Lock_Free_Try_Write_64 - (Ptr : Address; - Expected : in out uint64; - Desired : uint64) return Boolean - is - Actual : uint64; - - begin - if Expected /= Desired then - - if uint64'Atomic_Always_Lock_Free then - Actual := Sync_Compare_And_Swap_64 (Ptr, Expected, Desired); - else - raise Program_Error; - end if; - - if Actual /= Expected then - Expected := Actual; - return False; - end if; - end if; - - return True; - end Lock_Free_Try_Write_64; end System.Atomic_Primitives; diff --git a/gcc/ada/libgnat/s-atopri.ads b/gcc/ada/libgnat/s-atopri.ads index 891b2ed..ea03f1a 100644 --- a/gcc/ada/libgnat/s-atopri.ads +++ b/gcc/ada/libgnat/s-atopri.ads @@ -29,7 +29,7 @@ -- -- ------------------------------------------------------------------------------ --- This package contains both atomic primitives defined from gcc built-in +-- This package contains both atomic primitives defined from GCC built-in -- functions and operations used by the compiler to generate the lock-free -- implementation of protected objects. @@ -66,71 +66,31 @@ package System.Atomic_Primitives is -- GCC built-in atomic primitives -- ------------------------------------ - function Atomic_Load_8 + generic + type Atomic_Type is mod <>; + function Atomic_Load (Ptr : Address; - Model : Mem_Model := Seq_Cst) return uint8; - pragma Import (Intrinsic, Atomic_Load_8, "__atomic_load_1"); + Model : Mem_Model := Seq_Cst) return Atomic_Type; + pragma Import (Intrinsic, Atomic_Load, "__atomic_load_n"); - function Atomic_Load_16 - (Ptr : Address; - Model : Mem_Model := Seq_Cst) return uint16; - pragma Import (Intrinsic, Atomic_Load_16, "__atomic_load_2"); - - function Atomic_Load_32 - (Ptr : Address; - Model : Mem_Model := Seq_Cst) return uint32; - pragma Import (Intrinsic, Atomic_Load_32, "__atomic_load_4"); - - function Atomic_Load_64 - (Ptr : Address; - Model : Mem_Model := Seq_Cst) return uint64; - pragma Import (Intrinsic, Atomic_Load_64, "__atomic_load_8"); - - function Sync_Compare_And_Swap_8 - (Ptr : Address; - Expected : uint8; - Desired : uint8) return uint8; - pragma Import (Intrinsic, - Sync_Compare_And_Swap_8, - "__sync_val_compare_and_swap_1"); - - function Sync_Compare_And_Swap_16 - (Ptr : Address; - Expected : uint16; - Desired : uint16) return uint16; - pragma Import (Intrinsic, - Sync_Compare_And_Swap_16, - "__sync_val_compare_and_swap_2"); + function Atomic_Load_8 is new Atomic_Load (uint8); + function Atomic_Load_16 is new Atomic_Load (uint16); + function Atomic_Load_32 is new Atomic_Load (uint32); + function Atomic_Load_64 is new Atomic_Load (uint64); - function Sync_Compare_And_Swap_32 + generic + type Atomic_Type is mod <>; + function Sync_Compare_And_Swap (Ptr : Address; - Expected : uint32; - Desired : uint32) return uint32; - pragma Import (Intrinsic, - Sync_Compare_And_Swap_32, - "__sync_val_compare_and_swap_4"); + Expected : Atomic_Type; + Desired : Atomic_Type) return Atomic_Type; + pragma Import + (Intrinsic, Sync_Compare_And_Swap, "__sync_val_compare_and_swap"); - function Sync_Compare_And_Swap_64 - (Ptr : Address; - Expected : uint64; - Desired : uint64) return uint64; - pragma Import (Intrinsic, - Sync_Compare_And_Swap_64, - "__sync_val_compare_and_swap_8"); - - -- ??? We might want to switch to the __atomic series of builtins for - -- compare-and-swap operations at some point. - - -- function Atomic_Compare_Exchange_8 - -- (Ptr : Address; - -- Expected : Address; - -- Desired : uint8; - -- Weak : Boolean := False; - -- Success_Model : Mem_Model := Seq_Cst; - -- Failure_Model : Mem_Model := Seq_Cst) return Boolean; - -- pragma Import (Intrinsic, - -- Atomic_Compare_Exchange_8, - -- "__atomic_compare_exchange_1"); + function Sync_Compare_And_Swap_8 is new Sync_Compare_And_Swap (uint8); + function Sync_Compare_And_Swap_16 is new Sync_Compare_And_Swap (uint16); + function Sync_Compare_And_Swap_32 is new Sync_Compare_And_Swap (uint32); + function Sync_Compare_And_Swap_64 is new Sync_Compare_And_Swap (uint64); function Atomic_Test_And_Set (Ptr : System.Address; @@ -155,46 +115,37 @@ package System.Atomic_Primitives is -- The lock-free implementation uses two atomic instructions for the -- expansion of protected operations: - -- * Lock_Free_Read_N atomically loads the value of the protected component - -- accessed by the current protected operation. - - -- * Lock_Free_Try_Write_N tries to write the Desired value into Ptr only - -- if Expected and Desired mismatch. + -- * Lock_Free_Read atomically loads the value contained in Ptr (with the + -- Acquire synchronization mode). - function Lock_Free_Read_8 (Ptr : Address) return uint8; + -- * Lock_Free_Try_Write atomically tries to write the Desired value into + -- Ptr if Ptr contains the Expected value. It returns true if the value + -- in Ptr was changed, or False if it was not, in which case Expected is + -- updated to the unexpected value in Ptr. Note that it does nothing and + -- returns true if Desired and Expected are equal. - function Lock_Free_Read_16 (Ptr : Address) return uint16; + generic + type Atomic_Type is mod <>; + function Lock_Free_Read (Ptr : Address) return Atomic_Type; - function Lock_Free_Read_32 (Ptr : Address) return uint32; + function Lock_Free_Read_8 is new Lock_Free_Read (uint8); + function Lock_Free_Read_16 is new Lock_Free_Read (uint16); + function Lock_Free_Read_32 is new Lock_Free_Read (uint32); + function Lock_Free_Read_64 is new Lock_Free_Read (uint64); - function Lock_Free_Read_64 (Ptr : Address) return uint64; - - function Lock_Free_Try_Write_8 - (Ptr : Address; - Expected : in out uint8; - Desired : uint8) return Boolean; - - function Lock_Free_Try_Write_16 - (Ptr : Address; - Expected : in out uint16; - Desired : uint16) return Boolean; - - function Lock_Free_Try_Write_32 - (Ptr : Address; - Expected : in out uint32; - Desired : uint32) return Boolean; + generic + type Atomic_Type is mod <>; + function Lock_Free_Try_Write + (Ptr : Address; + Expected : in out Atomic_Type; + Desired : Atomic_Type) return Boolean; - function Lock_Free_Try_Write_64 - (Ptr : Address; - Expected : in out uint64; - Desired : uint64) return Boolean; + function Lock_Free_Try_Write_8 is new Lock_Free_Try_Write (uint8); + function Lock_Free_Try_Write_16 is new Lock_Free_Try_Write (uint16); + function Lock_Free_Try_Write_32 is new Lock_Free_Try_Write (uint32); + function Lock_Free_Try_Write_64 is new Lock_Free_Try_Write (uint64); - pragma Inline (Lock_Free_Read_8); - pragma Inline (Lock_Free_Read_16); - pragma Inline (Lock_Free_Read_32); - pragma Inline (Lock_Free_Read_64); - pragma Inline (Lock_Free_Try_Write_8); - pragma Inline (Lock_Free_Try_Write_16); - pragma Inline (Lock_Free_Try_Write_32); - pragma Inline (Lock_Free_Try_Write_64); +private + pragma Inline (Lock_Free_Read); + pragma Inline (Lock_Free_Try_Write); end System.Atomic_Primitives; diff --git a/gcc/ada/libgnat/s-parame.adb b/gcc/ada/libgnat/s-parame.adb index 9001626..09a65ee 100644 --- a/gcc/ada/libgnat/s-parame.adb +++ b/gcc/ada/libgnat/s-parame.adb @@ -55,7 +55,7 @@ package body System.Parameters is ------------------------ function Default_Stack_Size return Size_Type is - Default_Stack_Size : Integer; + Default_Stack_Size : constant Integer; pragma Import (C, Default_Stack_Size, "__gl_default_stack_size"); begin if Default_Stack_Size = -1 then diff --git a/gcc/ada/libgnat/s-parame__ae653.ads b/gcc/ada/libgnat/s-parame__ae653.ads deleted file mode 100644 index f838b41..0000000 --- a/gcc/ada/libgnat/s-parame__ae653.ads +++ /dev/null @@ -1,192 +0,0 @@ ------------------------------------------------------------------------------- --- -- --- GNAT COMPILER COMPONENTS -- --- -- --- S Y S T E M . P A R A M E T E R S -- --- -- --- S p e c -- --- -- --- Copyright (C) 1992-2021, 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- -- --- 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 -- --- <http://www.gnu.org/licenses/>. -- --- -- --- GNAT was originally developed by the GNAT team at New York University. -- --- Extensive contributions were provided by Ada Core Technologies Inc. -- --- -- ------------------------------------------------------------------------------- - --- Version is used by VxWorks 653, VxWorks MILS, and VxWorks6 cert Ravenscar - --- This package defines some system dependent parameters for GNAT. These --- are values that are referenced by the runtime library and are therefore --- relevant to the target machine. - --- The parameters whose value is defined in the spec are not generally --- expected to be changed. If they are changed, it will be necessary to --- recompile the run-time library. - --- The parameters which are defined by functions can be changed by modifying --- the body of System.Parameters in file s-parame.adb. A change to this body --- requires only rebinding and relinking of the application. - --- Note: do not introduce any pragma Inline statements into this unit, since --- otherwise the relinking and rebinding capability would be deactivated. - -package System.Parameters is - pragma Pure; - - --------------------------------------- - -- Task And Stack Allocation Control -- - --------------------------------------- - - type Size_Type is range - -(2 ** (Integer'(Standard'Address_Size) - 1)) .. - +(2 ** (Integer'(Standard'Address_Size) - 1)) - 1; - -- Type used to provide task stack sizes to the runtime. Sized to permit - -- stack sizes of up to half the total addressable memory space. This may - -- seem excessively large (even for 32-bit systems), however there are many - -- instances of users requiring large stack sizes (for example string - -- processing). - - Unspecified_Size : constant Size_Type := Size_Type'First; - -- Value used to indicate that no size type is set - - function Default_Stack_Size return Size_Type; - -- Default task stack size used if none is specified - - function Minimum_Stack_Size return Size_Type; - -- Minimum task stack size permitted - - function Adjust_Storage_Size (Size : Size_Type) return Size_Type; - -- Given the storage size stored in the TCB, return the Storage_Size - -- value required by the RM for the Storage_Size attribute. The - -- required adjustment is as follows: - -- - -- when Size = Unspecified_Size, return Default_Stack_Size - -- when Size < Minimum_Stack_Size, return Minimum_Stack_Size - -- otherwise return given Size - - Default_Env_Stack_Size : constant Size_Type := 14_336; - -- Assumed size of the environment task, if no other information - -- is available. This value is used when stack checking is - -- enabled and no GNAT_STACK_LIMIT environment variable is set. - -- This value is chosen as the VxWorks default stack size is 20kB, - -- and a little more than 4kB is necessary for the run time. - - Stack_Grows_Down : constant Boolean := True; - -- This constant indicates whether the stack grows up (False) or - -- down (True) in memory as functions are called. It is used for - -- proper implementation of the stack overflow check. - - Runtime_Default_Sec_Stack_Size : constant Size_Type := 10 * 1024; - -- The run-time chosen default size for secondary stacks that may be - -- overridden by the user with the use of binder -D switch. - - Sec_Stack_Dynamic : constant Boolean := False; - -- Indicates if secondary stacks can grow and shrink at run-time. If False, - -- the size of a secondary stack is fixed at the point of its creation. - - ------------------------------------ - -- Characteristics of time_t type -- - ------------------------------------ - - time_t_bits : constant := Long_Integer'Size; - -- Number of bits in type time_t - - ---------------------------------------------- - -- Characteristics of types in Interfaces.C -- - ---------------------------------------------- - - long_bits : constant := Long_Integer'Size; - -- Number of bits in type long and unsigned_long. The normal convention - -- is that this is the same as type Long_Integer, but this may not be true - -- of all targets. - - ptr_bits : constant := Standard'Address_Size; - subtype C_Address is System.Address; - -- Number of bits in Interfaces.C pointers, normally a standard address - - C_Malloc_Linkname : constant String := "__gnat_malloc"; - -- Name of runtime function used to allocate such a pointer - - ---------------------------------------------- - -- Behavior of Pragma Finalize_Storage_Only -- - ---------------------------------------------- - - -- Garbage_Collected is a Boolean constant whose value indicates the - -- effect of the pragma Finalize_Storage_Entry on a controlled type. - - -- Garbage_Collected = False - - -- The system releases all storage on program termination only, - -- but not other garbage collection occurs, so finalization calls - -- are omitted only for outer level objects can be omitted if - -- pragma Finalize_Storage_Only is used. - - -- Garbage_Collected = True - - -- The system provides full garbage collection, so it is never - -- necessary to release storage for controlled objects for which - -- a pragma Finalize_Storage_Only is used. - - Garbage_Collected : constant Boolean := False; - -- The storage mode for this system (release on program exit) - - --------------------- - -- Tasking Profile -- - --------------------- - - -- In the following sections, constant parameters are defined to - -- allow some optimizations and fine tuning within the tasking run time - -- based on restrictions on the tasking features. - - ------------------- - -- Task Abortion -- - ------------------- - - No_Abort : constant Boolean := False; - -- This constant indicates whether abort statements and asynchronous - -- transfer of control (ATC) are disallowed. If set to True, it is - -- assumed that neither construct is used, and the run time does not - -- need to defer/undefer abort and check for pending actions at - -- completion points. A value of True for No_Abort corresponds to: - -- pragma Restrictions (No_Abort_Statements); - -- pragma Restrictions (Max_Asynchronous_Select_Nesting => 0); - - --------------------- - -- Task Attributes -- - --------------------- - - Max_Attribute_Count : constant := 8; - -- Number of task attributes stored in the task control block - - ----------------------- - -- Task Image Length -- - ----------------------- - - Max_Task_Image_Length : constant := 32; - -- This constant specifies the maximum length of a task's image - - ------------------------------ - -- Exception Message Length -- - ------------------------------ - - Default_Exception_Msg_Max_Length : constant := 200; - -- This constant specifies the default number of characters to allow - -- in an exception message (200 is minimum required by RM 11.4.1(18)). - -end System.Parameters; diff --git a/gcc/ada/libgnat/s-parame__rtems.adb b/gcc/ada/libgnat/s-parame__rtems.adb index 1a6d577..ae88a2c 100644 --- a/gcc/ada/libgnat/s-parame__rtems.adb +++ b/gcc/ada/libgnat/s-parame__rtems.adb @@ -35,10 +35,6 @@ with Interfaces.C; package body System.Parameters is - function ada_pthread_minimum_stack_size return Interfaces.C.size_t; - pragma Import (C, ada_pthread_minimum_stack_size, - "_ada_pthread_minimum_stack_size"); - ------------------------- -- Adjust_Storage_Size -- ------------------------- @@ -61,8 +57,15 @@ package body System.Parameters is ------------------------ function Default_Stack_Size return Size_Type is + Default_Stack_Size : constant Integer + with Import, Convention => C, + External_Name => "__gl_default_stack_size"; begin - return Size_Type (ada_pthread_minimum_stack_size); + if Default_Stack_Size = -1 then + return 32 * 1024; + else + return Size_Type (Default_Stack_Size); + end if; end Default_Stack_Size; ------------------------ @@ -70,9 +73,11 @@ package body System.Parameters is ------------------------ function Minimum_Stack_Size return Size_Type is - + POSIX_Threads_Minimum_stack_size : constant Interfaces.C.size_t + with Import, Convention => C, + External_Name => "_POSIX_Threads_Minimum_stack_size"; begin - return Size_Type (ada_pthread_minimum_stack_size); + return Size_Type (POSIX_Threads_Minimum_stack_size); end Minimum_Stack_Size; end System.Parameters; diff --git a/gcc/ada/libgnat/s-parame__vxworks.adb b/gcc/ada/libgnat/s-parame__vxworks.adb index 5970eb0..45ee0a9 100644 --- a/gcc/ada/libgnat/s-parame__vxworks.adb +++ b/gcc/ada/libgnat/s-parame__vxworks.adb @@ -53,7 +53,7 @@ package body System.Parameters is ------------------------ function Default_Stack_Size return Size_Type is - Default_Stack_Size : Integer; + Default_Stack_Size : constant Integer; pragma Import (C, Default_Stack_Size, "__gl_default_stack_size"); begin if Default_Stack_Size = -1 then diff --git a/gcc/ada/libgnat/s-stchop__rtems.adb b/gcc/ada/libgnat/s-stchop__rtems.adb deleted file mode 100644 index f273f29..0000000 --- a/gcc/ada/libgnat/s-stchop__rtems.adb +++ /dev/null @@ -1,113 +0,0 @@ ------------------------------------------------------------------------------- --- -- --- GNAT RUN-TIME LIBRARY (GNARL) COMPONENTS -- --- -- --- S Y S T E M . S T A C K _ C H E C K I N G . O P E R A T I O N S -- --- -- --- B o d y -- --- -- --- Copyright (C) 1999-2021, Free Software Foundation, Inc. -- --- -- --- GNARL 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 -- --- <http://www.gnu.org/licenses/>. -- --- -- --- GNARL was developed by the GNARL team at Florida State University. -- --- Extensive contributions were provided by Ada Core Technologies, Inc. -- --- -- ------------------------------------------------------------------------------- - --- This is the RTEMS version of this package. --- This file should be kept synchronized with the general implementation --- provided by s-stchop.adb. - -pragma Restrictions (No_Elaboration_Code); --- We want to guarantee the absence of elaboration code because the --- binder does not handle references to this package. - -with Ada.Exceptions; - -with Interfaces.C; use Interfaces.C; - -package body System.Stack_Checking.Operations is - - ---------------------------- - -- Invalidate_Stack_Cache -- - ---------------------------- - - procedure Invalidate_Stack_Cache (Any_Stack : Stack_Access) is - pragma Warnings (Off, Any_Stack); - begin - Cache := Null_Stack; - end Invalidate_Stack_Cache; - - ----------------------------- - -- Notify_Stack_Attributes -- - ----------------------------- - - procedure Notify_Stack_Attributes - (Initial_SP : System.Address; - Size : System.Storage_Elements.Storage_Offset) - is - - -- RTEMS keeps all the information we need. - - pragma Unreferenced (Size); - pragma Unreferenced (Initial_SP); - - begin - null; - end Notify_Stack_Attributes; - - ----------------- - -- Stack_Check -- - ----------------- - - function Stack_Check - (Stack_Address : System.Address) return Stack_Access - is - pragma Unreferenced (Stack_Address); - - -- RTEMS has a routine to check if the stack is blown. - -- It returns a C99 bool. - function rtems_stack_checker_is_blown return Interfaces.C.unsigned_char; - pragma Import (C, - rtems_stack_checker_is_blown, "rtems_stack_checker_is_blown"); - - begin - -- RTEMS has a routine to check this. So use it. - - if rtems_stack_checker_is_blown /= 0 then - Ada.Exceptions.Raise_Exception - (E => Storage_Error'Identity, - Message => "stack overflow detected"); - end if; - - return null; - - end Stack_Check; - - ------------------------ - -- Update_Stack_Cache -- - ------------------------ - - procedure Update_Stack_Cache (Stack : Stack_Access) is - begin - if not Multi_Processor then - Cache := Stack; - end if; - end Update_Stack_Cache; - -end System.Stack_Checking.Operations; diff --git a/gcc/ada/libgnat/s-stratt.adb b/gcc/ada/libgnat/s-stratt.adb index 5f04153..d7f572e 100644 --- a/gcc/ada/libgnat/s-stratt.adb +++ b/gcc/ada/libgnat/s-stratt.adb @@ -36,13 +36,13 @@ with System.Stream_Attributes.XDR; package body System.Stream_Attributes is - XDR_Flag : Integer; - pragma Import (C, XDR_Flag, "__gl_xdr_stream"); + XDR_Stream : constant Integer; + pragma Import (C, XDR_Stream, "__gl_xdr_stream"); -- This imported value is used to determine whether the build had the -- binder switch "-xdr" present which enables XDR streaming and sets this -- flag to 1. - function XDR_Support return Boolean; + function XDR_Support return Boolean is (XDR_Stream = 1); pragma Inline (XDR_Support); -- Return True if XDR streaming should be used. Note that 128-bit integers -- are not supported by the XDR protocol and will raise Device_Error. @@ -142,15 +142,6 @@ package body System.Stream_Attributes is function To_WWC is new UC (S_WWC, Wide_Wide_Character); ----------------- - -- XDR_Support -- - ----------------- - - function XDR_Support return Boolean is - begin - return XDR_Flag = 1; - end XDR_Support; - - ----------------- -- Block_IO_OK -- ----------------- diff --git a/gcc/ada/libgnat/s-thread.ads b/gcc/ada/libgnat/s-thread.ads deleted file mode 100644 index 5d0a3c1..0000000 --- a/gcc/ada/libgnat/s-thread.ads +++ /dev/null @@ -1,92 +0,0 @@ ------------------------------------------------------------------------------- --- -- --- GNAT COMPILER COMPONENTS -- --- -- --- S Y S T E M . T H R E A D S -- --- -- --- S p e c -- --- -- --- Copyright (C) 1992-2021, 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- -- --- 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 -- --- <http://www.gnu.org/licenses/>. -- --- -- --- GNAT was originally developed by the GNAT team at New York University. -- --- Extensive contributions were provided by Ada Core Technologies Inc. -- --- -- ------------------------------------------------------------------------------- - --- This package provides facilities to register a thread to the runtime, --- and allocate its task specific datas. - --- This package is currently implemented for: - --- VxWorks AE653 rts-cert --- VxWorks AE653 rts-full (not rts-kernel) - -with Ada.Exceptions; -with Ada.Unchecked_Conversion; - -with Interfaces.C; - -with System.Secondary_Stack; -with System.Soft_Links; - -package System.Threads is - - package SST renames System.Secondary_Stack; - - type ATSD is limited private; - -- Type of the Ada thread specific data. It contains datas needed - -- by the GNAT runtime. - - type ATSD_Access is access ATSD; - function From_Address is - new Ada.Unchecked_Conversion (Address, ATSD_Access); - - subtype STATUS is Interfaces.C.int; - -- Equivalent of the C type STATUS - - type t_id is new Interfaces.C.long; - subtype Thread_Id is t_id; - - function Register (T : Thread_Id) return STATUS; - -- Create the task specific data necessary for Ada language support - - -------------------------- - -- Thread Body Handling -- - -------------------------- - - -- The subprograms in this section are called from the process body - -- wrapper in the APEX process registration package. - - procedure Thread_Body_Enter - (Sec_Stack_Ptr : SST.SS_Stack_Ptr; - Process_ATSD_Address : System.Address); - -- Enter thread body, see above for details - - procedure Thread_Body_Leave; - -- Leave thread body (normally), see above for details - - procedure Thread_Body_Exceptional_Exit - (EO : Ada.Exceptions.Exception_Occurrence); - -- Leave thread body (abnormally on exception), see above for details - -private - - type ATSD is new System.Soft_Links.TSD; - -end System.Threads; diff --git a/gcc/ada/libgnat/s-thread__ae653.adb b/gcc/ada/libgnat/s-thread__ae653.adb deleted file mode 100644 index ecbd415..0000000 --- a/gcc/ada/libgnat/s-thread__ae653.adb +++ /dev/null @@ -1,227 +0,0 @@ ------------------------------------------------------------------------------- --- -- --- GNAT COMPILER COMPONENTS -- --- -- --- S Y S T E M . T H R E A D S -- --- -- --- B o d y -- --- -- --- Copyright (C) 1992-2021, 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- -- --- 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 -- --- <http://www.gnu.org/licenses/>. -- --- -- --- GNAT was originally developed by the GNAT team at New York University. -- --- Extensive contributions were provided by Ada Core Technologies Inc. -- --- -- ------------------------------------------------------------------------------- - --- This is the VxWorks 653 version of this package - -pragma Restrictions (No_Tasking); --- The VxWorks 653 version of this package is intended only for programs --- which do not use Ada tasking. This restriction ensures that this --- will be checked by the binder. - -with System.Storage_Elements; use System.Storage_Elements; -with System.OS_Versions; use System.OS_Versions; - -package body System.Threads is - - use Interfaces.C; - - package SSL renames System.Soft_Links; - - Main_ATSD : aliased ATSD; - -- TSD for environment task - - Current_ATSD : aliased System.Address := System.Null_Address; - pragma Thread_Local_Storage (Current_ATSD); - -- pragma TLS needed since TaskVarAdd no longer available - - -- Assume guard pages for Helix APEX partitions, but leave - -- checking mechanism in for now, in case of surprises. ??? - Stack_Limit : Address; - pragma Import (C, Stack_Limit, "__gnat_stack_limit"); - - type Set_Stack_Limit_Proc_Acc is access procedure; - pragma Convention (C, Set_Stack_Limit_Proc_Acc); - - Set_Stack_Limit_Hook : Set_Stack_Limit_Proc_Acc; - pragma Import (C, Set_Stack_Limit_Hook, "__gnat_set_stack_limit_hook"); - -- Procedure to be called when a task is created to set stack limit if - -- limit checking is used. - - -- VxWorks specific API - - ERROR : constant STATUS := Interfaces.C.int (-1); - OK : constant STATUS := Interfaces.C.int (0); - - function taskIdVerify (tid : t_id) return STATUS; - pragma Import (C, taskIdVerify, "taskIdVerify"); - - function taskIdSelf return t_id; - pragma Import (C, taskIdSelf, "taskIdSelf"); - - ----------------------- - -- Local Subprograms -- - ----------------------- - - procedure Init_RTS; - -- This procedure performs the initialization of the run-time lib. - -- It installs System.Threads versions of certain operations of the - -- run-time lib. - - procedure Install_Handler; - pragma Import (C, Install_Handler, "__gnat_install_handler"); - - function Get_Sec_Stack return SST.SS_Stack_Ptr; - - procedure Set_Sec_Stack (Stack : SST.SS_Stack_Ptr); - - ----------------------- - -- Thread_Body_Enter -- - ----------------------- - - procedure Thread_Body_Enter - (Sec_Stack_Ptr : SST.SS_Stack_Ptr; - Process_ATSD_Address : System.Address) - is - - ATSD : constant ATSD_Access := From_Address (Process_ATSD_Address); - - begin - - ATSD.Sec_Stack_Ptr := Sec_Stack_Ptr; - SST.SS_Init (ATSD.Sec_Stack_Ptr); - Current_ATSD := Process_ATSD_Address; - Install_Handler; - - -- Assume guard pages for Helix/Vx7, but leave in for now ??? - -- Initialize stack limit if needed. - - if Current_ATSD /= Main_ATSD'Address - and then Set_Stack_Limit_Hook /= null - then - Set_Stack_Limit_Hook.all; - end if; - end Thread_Body_Enter; - - ---------------------------------- - -- Thread_Body_Exceptional_Exit -- - ---------------------------------- - - procedure Thread_Body_Exceptional_Exit - (EO : Ada.Exceptions.Exception_Occurrence) - is - pragma Unreferenced (EO); - - begin - -- No action for this target - - null; - end Thread_Body_Exceptional_Exit; - - ----------------------- - -- Thread_Body_Leave -- - ----------------------- - - procedure Thread_Body_Leave is - begin - -- No action for this target - - null; - end Thread_Body_Leave; - - -------------- - -- Init_RTS -- - -------------- - - procedure Init_RTS is - -- Register environment task - Result : constant Interfaces.C.int := Register (taskIdSelf); - pragma Assert (Result /= ERROR); - - begin - Main_ATSD.Sec_Stack_Ptr := SSL.Get_Sec_Stack_NT; - Current_ATSD := Main_ATSD'Address; - Install_Handler; - SSL.Get_Sec_Stack := Get_Sec_Stack'Access; - SSL.Set_Sec_Stack := Set_Sec_Stack'Access; - end Init_RTS; - - ------------------- - -- Get_Sec_Stack -- - ------------------- - - function Get_Sec_Stack return SST.SS_Stack_Ptr is - CTSD : constant ATSD_Access := From_Address (Current_ATSD); - begin - pragma Assert (CTSD /= null); - return CTSD.Sec_Stack_Ptr; - end Get_Sec_Stack; - - -------------- - -- Register -- - -------------- - - function Register (T : Thread_Id) return STATUS is - begin - -- It cannot be assumed that the caller of this routine has a ATSD; - -- so neither this procedure nor the procedures that it calls should - -- raise or handle exceptions, or make use of a secondary stack. - - if taskIdVerify (T) = ERROR then - return ERROR; - end if; - - Current_ATSD := To_Address (Integer_Address (T)); - - -- The same issue applies to the task variable that contains the stack - -- limit when that overflow checking mechanism is used instead of - -- probing. If stack checking is enabled and limit checking is used, - -- allocate the limit for this task. The environment task has this - -- initialized by the binder-generated main when - -- System.Stack_Check_Limits = True. - - pragma Warnings (Off); - - -- OS is a constant - if OS /= VxWorks_653 and then Set_Stack_Limit_Hook /= null then - -- Check that this is correct if limit checking left in. ??? - Stack_Limit := To_Address (Integer_Address (T)); - end if; - pragma Warnings (On); - - return OK; - end Register; - - ------------------- - -- Set_Sec_Stack -- - ------------------- - - procedure Set_Sec_Stack (Stack : SST.SS_Stack_Ptr) is - CTSD : constant ATSD_Access := From_Address (Current_ATSD); - begin - pragma Assert (CTSD /= null); - CTSD.Sec_Stack_Ptr := Stack; - end Set_Sec_Stack; - -begin - -- Initialize run-time library - - Init_RTS; -end System.Threads; diff --git a/gcc/ada/libgnat/s-trasym__dwarf.adb b/gcc/ada/libgnat/s-trasym__dwarf.adb index 61e7a1c..fb26d77 100644 --- a/gcc/ada/libgnat/s-trasym__dwarf.adb +++ b/gcc/ada/libgnat/s-trasym__dwarf.adb @@ -691,7 +691,7 @@ package body System.Traceback.Symbolic is return Symbolic_Traceback (E, Suppress_Hex => True); end Symbolic_Traceback_No_Hex; - Exception_Tracebacks_Symbolic : Integer; + Exception_Tracebacks_Symbolic : constant Integer; pragma Import (C, Exception_Tracebacks_Symbolic, diff --git a/gcc/ada/libgnat/s-widlllu.ads b/gcc/ada/libgnat/s-widlllu.ads index 018e740..10a0c9c 100644 --- a/gcc/ada/libgnat/s-widlllu.ads +++ b/gcc/ada/libgnat/s-widlllu.ads @@ -34,8 +34,9 @@ with System.Width_U; with System.Unsigned_Types; -package System.Wid_LLLU is - +package System.Wid_LLLU + with SPARK_Mode +is subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned; function Width_Long_Long_Long_Unsigned is diff --git a/gcc/ada/libgnat/s-widllu.ads b/gcc/ada/libgnat/s-widllu.ads index ab7ec58..7eaf966 100644 --- a/gcc/ada/libgnat/s-widllu.ads +++ b/gcc/ada/libgnat/s-widllu.ads @@ -34,8 +34,9 @@ with System.Width_U; with System.Unsigned_Types; -package System.Wid_LLU is - +package System.Wid_LLU + with SPARK_Mode +is subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned; function Width_Long_Long_Unsigned is new Width_U (Long_Long_Unsigned); diff --git a/gcc/ada/libgnat/s-widthu.adb b/gcc/ada/libgnat/s-widthu.adb index a91baec..fce8c7a 100644 --- a/gcc/ada/libgnat/s-widthu.adb +++ b/gcc/ada/libgnat/s-widthu.adb @@ -29,10 +29,87 @@ -- -- ------------------------------------------------------------------------------ +with Ada.Numerics.Big_Numbers.Big_Integers; +use Ada.Numerics.Big_Numbers.Big_Integers; + function System.Width_U (Lo, Hi : Uns) return Natural is + + -- Ghost code, loop invariants and assertions in this unit are meant for + -- analysis only, not for run-time checking, as it would be too costly + -- otherwise. This is enforced by setting the assertion policy to Ignore. + + pragma Assertion_Policy (Ghost => Ignore, + Loop_Invariant => Ignore, + Assert => Ignore); + W : Natural; T : Uns; + package Unsigned_Conversion is new Unsigned_Conversions (Int => Uns); + + function Big (Arg : Uns) return Big_Integer is + (Unsigned_Conversion.To_Big_Integer (Arg)) + with Ghost; + + -- Maximum value of exponent for 10 that fits in Uns'Base + function Max_Log10 return Natural is + (case Uns'Base'Size is + when 8 => 2, + when 16 => 4, + when 32 => 9, + when 64 => 19, + when 128 => 38, + when others => raise Program_Error) + with Ghost; + + Max_W : constant Natural := Max_Log10 with Ghost; + Big_10 : constant Big_Integer := Big (10) with Ghost; + + procedure Lemma_Lower_Mult (A, B, C : Big_Natural) + with + Ghost, + Pre => A <= B, + Post => A * C <= B * C; + + procedure Lemma_Div_Commutation (X, Y : Uns) + with + Ghost, + Pre => Y /= 0, + Post => Big (X) / Big (Y) = Big (X / Y); + + procedure Lemma_Div_Twice (X : Big_Natural; Y, Z : Big_Positive) + with + Ghost, + Post => X / Y / Z = X / (Y * Z); + + procedure Lemma_Lower_Mult (A, B, C : Big_Natural) is + begin + null; + end Lemma_Lower_Mult; + + procedure Lemma_Div_Commutation (X, Y : Uns) is + begin + null; + end Lemma_Div_Commutation; + + procedure Lemma_Div_Twice (X : Big_Natural; Y, Z : Big_Positive) is + XY : constant Big_Natural := X / Y; + YZ : constant Big_Natural := Y * Z; + XYZ : constant Big_Natural := X / Y / Z; + R : constant Big_Natural := (XY rem Z) * Y + (X rem Y); + begin + pragma Assert (X = XY * Y + (X rem Y)); + pragma Assert (XY = XY / Z * Z + (XY rem Z)); + pragma Assert (X = XYZ * YZ + R); + pragma Assert ((XY rem Z) * Y <= (Z - 1) * Y); + pragma Assert (R <= YZ - 1); + pragma Assert (X / YZ = (XYZ * YZ + R) / YZ); + pragma Assert (X / YZ = XYZ + R / YZ); + end Lemma_Div_Twice; + + Pow : Big_Integer := 1 with Ghost; + T_Init : constant Uns := Uns'Max (Lo, Hi) with Ghost; + begin if Lo > Hi then return 0; @@ -50,10 +127,43 @@ begin -- Increase value if more digits required while T >= 10 loop + Lemma_Div_Commutation (T, 10); + Lemma_Div_Twice (Big (T_Init), Big_10 ** (W - 2), Big_10); + T := T / 10; W := W + 1; + Pow := Pow * 10; + + pragma Loop_Invariant (W in 3 .. Max_W + 3); + pragma Loop_Invariant (Pow = Big_10 ** (W - 2)); + pragma Loop_Invariant (Big (T) = Big (T_Init) / Pow); + pragma Loop_Variant (Decreases => T); + pragma Annotate + (CodePeer, False_Positive, + "validity check", "confusion on generated code"); end loop; + declare + F : constant Big_Integer := Big_10 ** (W - 2) with Ghost; + Q : constant Big_Integer := Big (T_Init) / F with Ghost; + R : constant Big_Integer := Big (T_Init) rem F with Ghost; + begin + pragma Assert (Q < Big_10); + pragma Assert (Big (T_Init) = Q * F + R); + Lemma_Lower_Mult (Q, Big (9), F); + pragma Assert (Big (T_Init) <= Big (9) * F + F - 1); + pragma Assert (Big (T_Init) < Big_10 * F); + pragma Assert (Big_10 * F = Big_10 ** (W - 1)); + end; + + -- This is an expression of the functional postcondition for Width_U, + -- which cannot be expressed readily as a postcondition as this would + -- require making the instantiation Unsigned_Conversion and function + -- Big available from the spec. + + pragma Assert (Big (Lo) < Big_10 ** (W - 1)); + pragma Assert (Big (Hi) < Big_10 ** (W - 1)); + return W; end if; diff --git a/gcc/ada/libgnat/s-widuns.ads b/gcc/ada/libgnat/s-widuns.ads index 0528456..713532e 100644 --- a/gcc/ada/libgnat/s-widuns.ads +++ b/gcc/ada/libgnat/s-widuns.ads @@ -34,8 +34,9 @@ with System.Width_U; with System.Unsigned_Types; -package System.Wid_Uns is - +package System.Wid_Uns + with SPARK_Mode +is subtype Unsigned is Unsigned_Types.Unsigned; function Width_Unsigned is new Width_U (Unsigned); diff --git a/gcc/ada/libgnat/system-vxworks-ppc-ravenscar.ads b/gcc/ada/libgnat/system-vxworks-ppc-ravenscar.ads deleted file mode 100644 index b918c18..0000000 --- a/gcc/ada/libgnat/system-vxworks-ppc-ravenscar.ads +++ /dev/null @@ -1,185 +0,0 @@ ------------------------------------------------------------------------------- --- -- --- GNAT RUN-TIME COMPONENTS -- --- -- --- S Y S T E M -- --- -- --- S p e c -- --- (VxWorks/HIE Ravenscar Version PPC) -- --- -- --- Copyright (C) 1992-2021, 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 -- --- <http://www.gnu.org/licenses/>. -- --- -- --- GNAT was originally developed by the GNAT team at New York University. -- --- Extensive contributions were provided by Ada Core Technologies Inc. -- --- -- ------------------------------------------------------------------------------- - --- This is a Ravenscar VxWorks version of this package for PowerPC targets - -pragma Restrictions (No_Exception_Propagation); --- Only local exception handling is supported in this profile - -pragma Restrictions (No_Exception_Registration); --- Disable exception name registration. This capability is not used because --- it is only required by exception stream attributes which are not supported --- in this run time. - -pragma Restrictions (No_Implicit_Dynamic_Code); --- Pointers to nested subprograms are not allowed in this run time, in order --- to prevent the compiler from building "trampolines". - -pragma Restrictions (No_Finalization); --- Controlled types are not supported in this run time - -pragma Profile (Ravenscar); --- This is a Ravenscar run time - -pragma Discard_Names; --- Disable explicitly the generation of names associated with entities in --- order to reduce the amount of storage used. These names are not used anyway --- (attributes such as 'Image and 'Value are not supported in this run time). - -package System is - pragma Pure; - -- Note that we take advantage of the implementation permission to make - -- this unit Pure instead of Preelaborable; see RM 13.7.1(15). In Ada - -- 2005, this is Pure in any case (AI-362). - - pragma No_Elaboration_Code_All; - -- Allow the use of that restriction in units that WITH this unit - - type Name is (SYSTEM_NAME_GNAT); - System_Name : constant Name := SYSTEM_NAME_GNAT; - - -- System-Dependent Named Numbers - - Min_Int : constant := -2 ** (Standard'Max_Integer_Size - 1); - Max_Int : constant := 2 ** (Standard'Max_Integer_Size - 1) - 1; - - Max_Binary_Modulus : constant := 2 ** Standard'Max_Integer_Size; - Max_Nonbinary_Modulus : constant := 2 ** Integer'Size - 1; - - Max_Base_Digits : constant := Long_Long_Float'Digits; - Max_Digits : constant := Long_Long_Float'Digits; - - Max_Mantissa : constant := Standard'Max_Integer_Size - 1; - Fine_Delta : constant := 2.0 ** (-Max_Mantissa); - - Tick : constant := 1.0 / 60.0; - - -- Storage-related Declarations - - type Address is private; - pragma Preelaborable_Initialization (Address); - Null_Address : constant Address; - - Storage_Unit : constant := 8; - Word_Size : constant := 32; - Memory_Size : constant := 2 ** 32; - - -- Address comparison - - function "<" (Left, Right : Address) return Boolean; - function "<=" (Left, Right : Address) return Boolean; - function ">" (Left, Right : Address) return Boolean; - function ">=" (Left, Right : Address) return Boolean; - function "=" (Left, Right : Address) return Boolean; - - pragma Import (Intrinsic, "<"); - pragma Import (Intrinsic, "<="); - pragma Import (Intrinsic, ">"); - pragma Import (Intrinsic, ">="); - pragma Import (Intrinsic, "="); - - -- Other System-Dependent Declarations - - type Bit_Order is (High_Order_First, Low_Order_First); - Default_Bit_Order : constant Bit_Order := High_Order_First; - pragma Warnings (Off, Default_Bit_Order); -- kill constant condition warning - - -- Priority-related Declarations (RM D.1) - - -- Ada priorities are mapped to VxWorks priorities using the following - -- transformation: 255 - Ada Priority - - -- Ada priorities are used as follows: - - -- 256 is reserved for the VxWorks kernel - -- 248 - 255 correspond to hardware interrupt levels 0 .. 7 - -- 247 is a catchall default "interrupt" priority for signals, - -- allowing higher priority than normal tasks, but lower than - -- hardware priority levels. Protected Object ceilings can - -- override these values. - -- 246 is used by the Interrupt_Manager task - - Max_Priority : constant Positive := 245; - Max_Interrupt_Priority : constant Positive := 255; - - subtype Any_Priority is Integer range 0 .. 255; - subtype Priority is Any_Priority range 0 .. 245; - subtype Interrupt_Priority is Any_Priority range 246 .. 255; - - Default_Priority : constant Priority := 122; - -private - - type Address is mod Memory_Size; - Null_Address : constant Address := 0; - - -------------------------------------- - -- System Implementation Parameters -- - -------------------------------------- - - -- These parameters provide information about the target that is used - -- by the compiler. They are in the private part of System, where they - -- can be accessed using the special circuitry in the Targparm unit - -- whose source should be consulted for more detailed descriptions - -- of the individual switch values. - - Backend_Divide_Checks : constant Boolean := False; - Backend_Overflow_Checks : constant Boolean := True; - Command_Line_Args : constant Boolean := False; - Configurable_Run_Time : constant Boolean := True; - Denorm : constant Boolean := True; - Duration_32_Bits : constant Boolean := True; - Exit_Status_Supported : constant Boolean := True; - Machine_Overflows : constant Boolean := True; - Machine_Rounds : constant Boolean := True; - Preallocated_Stacks : constant Boolean := False; - Signed_Zeros : constant Boolean := True; - Stack_Check_Default : constant Boolean := False; - Stack_Check_Probes : constant Boolean := False; - Stack_Check_Limits : constant Boolean := True; - Support_Aggregates : constant Boolean := True; - Support_Composite_Assign : constant Boolean := True; - Support_Composite_Compare : constant Boolean := True; - Support_Long_Shifts : constant Boolean := True; - Always_Compatible_Rep : constant Boolean := True; - Suppress_Standard_Library : constant Boolean := True; - Use_Ada_Main_Program_Name : constant Boolean := True; - Frontend_Exceptions : constant Boolean := True; - ZCX_By_Default : constant Boolean := False; - - Executable_Extension : constant String := ".out"; - -end System; diff --git a/gcc/ada/libgnat/system-vxworks-ppc.ads b/gcc/ada/libgnat/system-vxworks-ppc.ads deleted file mode 100644 index 8f384e9..0000000 --- a/gcc/ada/libgnat/system-vxworks-ppc.ads +++ /dev/null @@ -1,163 +0,0 @@ ------------------------------------------------------------------------------- --- -- --- GNAT RUN-TIME COMPONENTS -- --- -- --- S Y S T E M -- --- -- --- S p e c -- --- (VxWorks 5 Version PPC) -- --- -- --- Copyright (C) 1992-2021, 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 -- --- <http://www.gnu.org/licenses/>. -- --- -- --- GNAT was originally developed by the GNAT team at New York University. -- --- Extensive contributions were provided by Ada Core Technologies Inc. -- --- -- ------------------------------------------------------------------------------- - -package System is - pragma Pure; - -- Note that we take advantage of the implementation permission to make - -- this unit Pure instead of Preelaborable; see RM 13.7.1(15). In Ada - -- 2005, this is Pure in any case (AI-362). - - pragma No_Elaboration_Code_All; - -- Allow the use of that restriction in units that WITH this unit - - type Name is (SYSTEM_NAME_GNAT); - System_Name : constant Name := SYSTEM_NAME_GNAT; - - -- System-Dependent Named Numbers - - Min_Int : constant := -2 ** (Standard'Max_Integer_Size - 1); - Max_Int : constant := 2 ** (Standard'Max_Integer_Size - 1) - 1; - - Max_Binary_Modulus : constant := 2 ** Standard'Max_Integer_Size; - Max_Nonbinary_Modulus : constant := 2 ** Integer'Size - 1; - - Max_Base_Digits : constant := Long_Long_Float'Digits; - Max_Digits : constant := Long_Long_Float'Digits; - - Max_Mantissa : constant := Standard'Max_Integer_Size - 1; - Fine_Delta : constant := 2.0 ** (-Max_Mantissa); - - Tick : constant := 1.0 / 60.0; - - -- Storage-related Declarations - - type Address is private; - pragma Preelaborable_Initialization (Address); - Null_Address : constant Address; - - Storage_Unit : constant := 8; - Word_Size : constant := 32; - Memory_Size : constant := 2 ** 32; - - -- Address comparison - - function "<" (Left, Right : Address) return Boolean; - function "<=" (Left, Right : Address) return Boolean; - function ">" (Left, Right : Address) return Boolean; - function ">=" (Left, Right : Address) return Boolean; - function "=" (Left, Right : Address) return Boolean; - - pragma Import (Intrinsic, "<"); - pragma Import (Intrinsic, "<="); - pragma Import (Intrinsic, ">"); - pragma Import (Intrinsic, ">="); - pragma Import (Intrinsic, "="); - - -- Other System-Dependent Declarations - - type Bit_Order is (High_Order_First, Low_Order_First); - Default_Bit_Order : constant Bit_Order := High_Order_First; - pragma Warnings (Off, Default_Bit_Order); -- kill constant condition warning - - -- Priority-related Declarations (RM D.1) - - -- Ada priorities are mapped to VxWorks priorities using the following - -- transformation: 255 - Ada Priority - - -- Ada priorities are used as follows: - - -- 256 is reserved for the VxWorks kernel - -- 248 - 255 correspond to hardware interrupt levels 0 .. 7 - -- 247 is a catchall default "interrupt" priority for signals, - -- allowing higher priority than normal tasks, but lower than - -- hardware priority levels. Protected Object ceilings can - -- override these values. - -- 246 is used by the Interrupt_Manager task - - Max_Priority : constant Positive := 245; - Max_Interrupt_Priority : constant Positive := 255; - - subtype Any_Priority is Integer range 0 .. 255; - subtype Priority is Any_Priority range 0 .. 245; - subtype Interrupt_Priority is Any_Priority range 246 .. 255; - - Default_Priority : constant Priority := 122; - -private - - pragma Linker_Options ("--specs=vxworks-ppc-link.spec"); - -- Setup proper set of -L's for this configuration - - type Address is mod Memory_Size; - Null_Address : constant Address := 0; - - -------------------------------------- - -- System Implementation Parameters -- - -------------------------------------- - - -- These parameters provide information about the target that is used - -- by the compiler. They are in the private part of System, where they - -- can be accessed using the special circuitry in the Targparm unit - -- whose source should be consulted for more detailed descriptions - -- of the individual switch values. - - Backend_Divide_Checks : constant Boolean := False; - Backend_Overflow_Checks : constant Boolean := True; - Command_Line_Args : constant Boolean := False; - Configurable_Run_Time : constant Boolean := False; - Denorm : constant Boolean := True; - Duration_32_Bits : constant Boolean := False; - Exit_Status_Supported : constant Boolean := True; - Machine_Overflows : constant Boolean := False; - Machine_Rounds : constant Boolean := True; - Preallocated_Stacks : constant Boolean := False; - Signed_Zeros : constant Boolean := True; - Stack_Check_Default : constant Boolean := False; - Stack_Check_Probes : constant Boolean := False; - Stack_Check_Limits : constant Boolean := True; - Support_Aggregates : constant Boolean := True; - Support_Composite_Assign : constant Boolean := True; - Support_Composite_Compare : constant Boolean := True; - Support_Long_Shifts : constant Boolean := True; - Always_Compatible_Rep : constant Boolean := False; - Suppress_Standard_Library : constant Boolean := False; - Use_Ada_Main_Program_Name : constant Boolean := True; - Frontend_Exceptions : constant Boolean := True; - ZCX_By_Default : constant Boolean := False; - - Executable_Extension : constant String := ".out"; - -end System; diff --git a/gcc/ada/libgnat/system-vxworks-x86.ads b/gcc/ada/libgnat/system-vxworks-x86.ads deleted file mode 100644 index 6f952a2..0000000 --- a/gcc/ada/libgnat/system-vxworks-x86.ads +++ /dev/null @@ -1,164 +0,0 @@ ------------------------------------------------------------------------------- --- -- --- GNAT RUN-TIME COMPONENTS -- --- -- --- S Y S T E M -- --- -- --- S p e c -- --- (VxWorks 5 Version x86) -- --- -- --- Copyright (C) 1992-2021, 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 -- --- <http://www.gnu.org/licenses/>. -- --- -- --- GNAT was originally developed by the GNAT team at New York University. -- --- Extensive contributions were provided by Ada Core Technologies Inc. -- --- -- ------------------------------------------------------------------------------- - -package System is - pragma Pure; - -- Note that we take advantage of the implementation permission to make - -- this unit Pure instead of Preelaborable; see RM 13.7.1(15). In Ada - -- 2005, this is Pure in any case (AI-362). - - pragma No_Elaboration_Code_All; - -- Allow the use of that restriction in units that WITH this unit - - type Name is (SYSTEM_NAME_GNAT); - System_Name : constant Name := SYSTEM_NAME_GNAT; - - -- System-Dependent Named Numbers - - Min_Int : constant := -2 ** (Standard'Max_Integer_Size - 1); - Max_Int : constant := 2 ** (Standard'Max_Integer_Size - 1) - 1; - - Max_Binary_Modulus : constant := 2 ** Standard'Max_Integer_Size; - Max_Nonbinary_Modulus : constant := 2 ** Integer'Size - 1; - - Max_Base_Digits : constant := Long_Long_Float'Digits; - Max_Digits : constant := Long_Long_Float'Digits; - - Max_Mantissa : constant := Standard'Max_Integer_Size - 1; - Fine_Delta : constant := 2.0 ** (-Max_Mantissa); - - Tick : constant := 1.0 / 60.0; - - -- Storage-related Declarations - - type Address is private; - pragma Preelaborable_Initialization (Address); - Null_Address : constant Address; - - Storage_Unit : constant := 8; - Word_Size : constant := 32; - Memory_Size : constant := 2 ** 32; - - -- Address comparison - - function "<" (Left, Right : Address) return Boolean; - function "<=" (Left, Right : Address) return Boolean; - function ">" (Left, Right : Address) return Boolean; - function ">=" (Left, Right : Address) return Boolean; - function "=" (Left, Right : Address) return Boolean; - - pragma Import (Intrinsic, "<"); - pragma Import (Intrinsic, "<="); - pragma Import (Intrinsic, ">"); - pragma Import (Intrinsic, ">="); - pragma Import (Intrinsic, "="); - - -- Other System-Dependent Declarations - - type Bit_Order is (High_Order_First, Low_Order_First); - Default_Bit_Order : constant Bit_Order := Low_Order_First; - pragma Warnings (Off, Default_Bit_Order); -- kill constant condition warning - - -- Priority-related Declarations (RM D.1) - - -- Ada priorities are mapped to VxWorks priorities using the following - -- transformation: 255 - Ada Priority - - -- Ada priorities are used as follows: - - -- 256 is reserved for the VxWorks kernel - -- 248 - 255 correspond to hardware interrupt levels 0 .. 7 - -- 247 is a catchall default "interrupt" priority for signals, - -- allowing higher priority than normal tasks, but lower than - -- hardware priority levels. Protected Object ceilings can - -- override these values. - -- 246 is used by the Interrupt_Manager task - - Max_Priority : constant Positive := 245; - Max_Interrupt_Priority : constant Positive := 255; - - subtype Any_Priority is Integer range 0 .. 255; - subtype Priority is Any_Priority range 0 .. 245; - subtype Interrupt_Priority is Any_Priority range 246 .. 255; - - Default_Priority : constant Priority := 122; - -private - - pragma Linker_Options ("--specs=vxworks-x86-link.spec"); - -- Setup proper set of -L's for this configuration - - type Address is mod Memory_Size; - Null_Address : constant Address := 0; - - -------------------------------------- - -- System Implementation Parameters -- - -------------------------------------- - - -- These parameters provide information about the target that is used - -- by the compiler. They are in the private part of System, where they - -- can be accessed using the special circuitry in the Targparm unit - -- whose source should be consulted for more detailed descriptions - -- of the individual switch values. - - Backend_Divide_Checks : constant Boolean := False; - Backend_Overflow_Checks : constant Boolean := True; - Command_Line_Args : constant Boolean := False; - Configurable_Run_Time : constant Boolean := False; - Denorm : constant Boolean := True; - Duration_32_Bits : constant Boolean := False; - Exit_Status_Supported : constant Boolean := True; - Machine_Overflows : constant Boolean := False; - Machine_Rounds : constant Boolean := True; - Preallocated_Stacks : constant Boolean := False; - Signed_Zeros : constant Boolean := True; - Stack_Check_Default : constant Boolean := False; - Stack_Check_Probes : constant Boolean := False; - Stack_Check_Limits : constant Boolean := True; - Support_Aggregates : constant Boolean := True; - Support_Atomic_Primitives : constant Boolean := True; - Support_Composite_Assign : constant Boolean := True; - Support_Composite_Compare : constant Boolean := True; - Support_Long_Shifts : constant Boolean := True; - Always_Compatible_Rep : constant Boolean := False; - Suppress_Standard_Library : constant Boolean := False; - Use_Ada_Main_Program_Name : constant Boolean := True; - Frontend_Exceptions : constant Boolean := True; - ZCX_By_Default : constant Boolean := False; - - Executable_Extension : constant String := ".out"; - -end System; |