diff options
| author | Ian Lance Taylor <iant@golang.org> | 2023-06-21 11:04:04 -0700 |
|---|---|---|
| committer | Ian Lance Taylor <iant@golang.org> | 2023-06-21 11:04:04 -0700 |
| commit | 97e31a0a2a2d2273687fcdb4e5416aab1a2186e1 (patch) | |
| tree | d5c1cae4de436a0fe54a5f0a2a197d309f3d654c /gcc/ada/libgnat | |
| parent | 6612f4f8cb9b0d5af18ec69ad04e56debc3e6ced (diff) | |
| parent | 577223aebc7acdd31e62b33c1682fe54a622ae27 (diff) | |
| download | gcc-97e31a0a2a2d2273687fcdb4e5416aab1a2186e1.zip gcc-97e31a0a2a2d2273687fcdb4e5416aab1a2186e1.tar.gz gcc-97e31a0a2a2d2273687fcdb4e5416aab1a2186e1.tar.bz2 | |
Merge from trunk revision 577223aebc7acdd31e62b33c1682fe54a622ae27.
Diffstat (limited to 'gcc/ada/libgnat')
142 files changed, 1978 insertions, 1382 deletions
diff --git a/gcc/ada/libgnat/a-calend.ads b/gcc/ada/libgnat/a-calend.ads index 2771cb5..d67bf07 100644 --- a/gcc/ada/libgnat/a-calend.ads +++ b/gcc/ada/libgnat/a-calend.ads @@ -102,16 +102,16 @@ is function "+" (Left : Time; Right : Duration) return Time with - Global => null; + SPARK_Mode => Off; function "+" (Left : Duration; Right : Time) return Time with - Global => null; + SPARK_Mode => Off; function "-" (Left : Time; Right : Duration) return Time with - Global => null; + SPARK_Mode => Off; function "-" (Left : Time; Right : Time) return Duration with - Global => null; + SPARK_Mode => Off; -- The first three functions will raise Time_Error if the resulting time -- value is less than the start of Ada time in UTC or greater than the -- end of Ada time in UTC. The last function will raise Time_Error if the diff --git a/gcc/ada/libgnat/a-calfor.adb b/gcc/ada/libgnat/a-calfor.adb index 3325e56..18f4e73 100644 --- a/gcc/ada/libgnat/a-calfor.adb +++ b/gcc/ada/libgnat/a-calfor.adb @@ -590,10 +590,6 @@ package body Ada.Calendar.Formatting is Leap_Second : Boolean := False; Time_Zone : Time_Zones.Time_Offset := 0) return Time is - Adj_Year : Year_Number := Year; - Adj_Month : Month_Number := Month; - Adj_Day : Day_Number := Day; - H : constant Integer := 1; M : constant Integer := 1; Se : constant Integer := 1; @@ -612,32 +608,11 @@ package body Ada.Calendar.Formatting is raise Constraint_Error; end if; - -- A Seconds value of 86_400 denotes a new day. This case requires an - -- adjustment to the input values. - - if Seconds = 86_400.0 then - if Day < Days_In_Month (Month) - or else (Is_Leap (Year) - and then Month = 2) - then - Adj_Day := Day + 1; - else - Adj_Day := 1; - - if Month < 12 then - Adj_Month := Month + 1; - else - Adj_Month := 1; - Adj_Year := Year + 1; - end if; - end if; - end if; - return Formatting_Operations.Time_Of - (Year => Adj_Year, - Month => Adj_Month, - Day => Adj_Day, + (Year => Year, + Month => Month, + Day => Day, Day_Secs => Seconds, Hour => H, Minute => M, diff --git a/gcc/ada/libgnat/a-cbdlli.ads b/gcc/ada/libgnat/a-cbdlli.ads index 961a007..b881053 100644 --- a/gcc/ada/libgnat/a-cbdlli.ads +++ b/gcc/ada/libgnat/a-cbdlli.ads @@ -276,12 +276,12 @@ private type Node_Array is array (Count_Type range <>) of Node_Type; type List (Capacity : Count_Type) is tagged record - Nodes : Node_Array (1 .. Capacity); Free : Count_Type'Base := -1; First : Count_Type := 0; Last : Count_Type := 0; Length : Count_Type := 0; TC : aliased Tamper_Counts; + Nodes : Node_Array (1 .. Capacity); end record with Put_Image => Put_Image; procedure Put_Image diff --git a/gcc/ada/libgnat/a-chahan.ads b/gcc/ada/libgnat/a-chahan.ads index 159cd70..89b2d68 100644 --- a/gcc/ada/libgnat/a-chahan.ads +++ b/gcc/ada/libgnat/a-chahan.ads @@ -40,14 +40,13 @@ pragma Assertion_Policy (Post => Ignore); with Ada.Characters.Latin_1; -package Ada.Characters.Handling - with SPARK_Mode +package Ada.Characters.Handling with + SPARK_Mode, + Always_Terminates is pragma Pure; -- In accordance with Ada 2005 AI-362 - pragma Annotate (GNATprove, Always_Return, Handling); - ---------------------------------------- -- Character Classification Functions -- ---------------------------------------- diff --git a/gcc/ada/libgnat/a-cidlli.adb b/gcc/ada/libgnat/a-cidlli.adb index 65582d1..9e6ad70 100644 --- a/gcc/ada/libgnat/a-cidlli.adb +++ b/gcc/ada/libgnat/a-cidlli.adb @@ -1283,22 +1283,19 @@ is is First_Time : Boolean := True; use System.Put_Images; + begin + Array_Before (S); - procedure Put_Elem (Position : Cursor); - procedure Put_Elem (Position : Cursor) is - begin + for X of V loop if First_Time then First_Time := False; else Simple_Array_Between (S); end if; - Element_Type'Put_Image (S, Element (Position)); - end Put_Elem; + Element_Type'Put_Image (S, X); + end loop; - begin - Array_Before (S); - Iterate (V, Put_Elem'Access); Array_After (S); end Put_Image; diff --git a/gcc/ada/libgnat/a-coinho__shared.adb b/gcc/ada/libgnat/a-coinho__shared.adb index 3670890..f49ac4a 100644 --- a/gcc/ada/libgnat/a-coinho__shared.adb +++ b/gcc/ada/libgnat/a-coinho__shared.adb @@ -149,8 +149,6 @@ package body Ada.Containers.Indefinite_Holders is raise Constraint_Error with "container is empty"; end if; - Detach (Container); - declare Ref : constant Constant_Reference_Type := (Element => Container.Reference.Element.all'Access, @@ -305,8 +303,6 @@ package body Ada.Containers.Indefinite_Holders is raise Constraint_Error with "container is empty"; end if; - Detach (Container); - B := B + 1; begin diff --git a/gcc/ada/libgnat/a-coinve.adb b/gcc/ada/libgnat/a-coinve.adb index 846f819..dd0e8cd 100644 --- a/gcc/ada/libgnat/a-coinve.adb +++ b/gcc/ada/libgnat/a-coinve.adb @@ -2679,22 +2679,19 @@ is is First_Time : Boolean := True; use System.Put_Images; + begin + Array_Before (S); - procedure Put_Elem (Position : Cursor); - procedure Put_Elem (Position : Cursor) is - begin + for X of V loop if First_Time then First_Time := False; else Simple_Array_Between (S); end if; - Element_Type'Put_Image (S, Element (Position)); - end Put_Elem; + Element_Type'Put_Image (S, X); + end loop; - begin - Array_Before (S); - Iterate (V, Put_Elem'Access); Array_After (S); end Put_Image; diff --git a/gcc/ada/libgnat/a-costso.adb b/gcc/ada/libgnat/a-costso.adb index fcdd7aa..fb4da32 100644 --- a/gcc/ada/libgnat/a-costso.adb +++ b/gcc/ada/libgnat/a-costso.adb @@ -124,7 +124,7 @@ package body Ada.Containers.Stable_Sorting is -- Start of processing for Merge_Parts begin - while (P1.Length /= 0) or (P2.Length /= 0) loop + while P1.Length /= 0 or P2.Length /= 0 loop if P1.Length = 0 then Take_From_P2 := True; elsif P2.Length = 0 then diff --git a/gcc/ada/libgnat/a-crdlli.ads b/gcc/ada/libgnat/a-crdlli.ads index d9c4517..fa4fe15 100644 --- a/gcc/ada/libgnat/a-crdlli.ads +++ b/gcc/ada/libgnat/a-crdlli.ads @@ -314,11 +314,11 @@ private type Node_Array is array (Count_Type range <>) of Node_Type; type List (Capacity : Count_Type) is tagged limited record - Nodes : Node_Array (1 .. Capacity); Free : Count_Type'Base := -1; First : Count_Type := 0; Last : Count_Type := 0; Length : Count_Type := 0; + Nodes : Node_Array (1 .. Capacity); end record; type List_Access is access all List; diff --git a/gcc/ada/libgnat/a-dhfina.adb b/gcc/ada/libgnat/a-dhfina.adb index a7e9e386b..9435cc0 100644 --- a/gcc/ada/libgnat/a-dhfina.adb +++ b/gcc/ada/libgnat/a-dhfina.adb @@ -307,7 +307,7 @@ package body Ada.Directories.Hierarchical_File_Names is -- Check that directory is valid if Separated_Dir /= "" - and then (not Is_Valid_Path_Name (Separated_Dir & Relative_Name)) + and then not Is_Valid_Path_Name (Separated_Dir & Relative_Name) then raise Name_Error with "invalid path composition """ & Separated_Dir & Relative_Name & '"'; diff --git a/gcc/ada/libgnat/a-direct.adb b/gcc/ada/libgnat/a-direct.adb index d660b69..4b08d41 100644 --- a/gcc/ada/libgnat/a-direct.adb +++ b/gcc/ada/libgnat/a-direct.adb @@ -176,9 +176,7 @@ package body Ada.Directories is raise Name_Error with "invalid directory path name """ & Containing_Directory & '"'; - elsif - Extension'Length = 0 and then (not Is_Valid_Simple_Name (Name)) - then + elsif Extension'Length = 0 and then not Is_Valid_Simple_Name (Name) then raise Name_Error with "invalid simple name """ & Name & '"'; diff --git a/gcc/ada/libgnat/a-excach.adb b/gcc/ada/libgnat/a-excach.adb index 840da0c..784194d 100644 --- a/gcc/ada/libgnat/a-excach.adb +++ b/gcc/ada/libgnat/a-excach.adb @@ -66,8 +66,8 @@ begin (Traceback => Excep.Tracebacks, Max_Len => Max_Tracebacks, Len => Excep.Num_Tracebacks, - Exclude_Min => Code_Address_For_AAA, - Exclude_Max => Code_Address_For_ZZZ, + Exclude_Min => AAA'Code_Address, + Exclude_Max => ZZZ'Code_Address, Skip_Frames => 3); end if; diff --git a/gcc/ada/libgnat/a-except.adb b/gcc/ada/libgnat/a-except.adb index 7d728d6..20a7736 100644 --- a/gcc/ada/libgnat/a-except.adb +++ b/gcc/ada/libgnat/a-except.adb @@ -65,29 +65,32 @@ package body Ada.Exceptions is -- from C clients using the given external name, even though they are not -- technically visible in the Ada sense. - function Code_Address_For_AAA return System.Address; - function Code_Address_For_ZZZ return System.Address; - -- Return start and end of procedures in this package + procedure AAA; + procedure ZZZ; + -- Start and end of procedures in this package -- - -- These procedures are used to provide exclusion bounds in - -- calls to Call_Chain at exception raise points from this unit. The - -- purpose is to arrange for the exception tracebacks not to include - -- frames from subprograms involved in the raise process, as these are - -- meaningless from the user's standpoint. + -- These procedures are used to provide exclusion bounds in calls to + -- Call_Chain at exception raise points from this unit. The purpose is + -- to arrange for the exception tracebacks not to include frames from + -- subprograms involved in the raise process, as these are meaningless + -- from the user's standpoint. -- -- For these bounds to be meaningful, we need to ensure that the object - -- code for the subprograms involved in processing a raise is located - -- after the object code Code_Address_For_AAA and before the object - -- code Code_Address_For_ZZZ. This will indeed be the case as long as - -- the following rules are respected: + -- code for the subprograms involved in processing a raise is located after + -- the object code AAA and before the object code ZZZ. This will indeed be + -- the case as long as the following rules are respected: -- -- 1) The bodies of the subprograms involved in processing a raise - -- are located after the body of Code_Address_For_AAA and before the - -- body of Code_Address_For_ZZZ. + -- are located after the body of AAA and before the body of ZZZ. -- -- 2) No pragma Inline applies to any of these subprograms, as this -- could delay the corresponding assembly output until the end of -- the unit. + -- + -- To obtain the address of AAA and ZZZ, use the Code_Address attribute + -- instead of the Address attribute as the latter will return the address + -- of a stub or descriptor on some platforms. This include IA-64, + -- PowerPC/AIX, big-endian PowerPC64 and HPUX. procedure Call_Chain (Excep : EOA); -- Store up to Max_Tracebacks in Excep, corresponding to the current @@ -771,24 +774,15 @@ package body Ada.Exceptions is Rmsg_36 : constant String := "stream operation not allowed" & NUL; Rmsg_37 : constant String := "build-in-place mismatch" & NUL; - -------------------------- - -- Code_Address_For_AAA -- - -------------------------- + --------- + -- AAA -- + --------- -- This function gives us the start of the PC range for addresses within -- the exception unit itself. We hope that gigi/gcc keep all the procedures -- in their original order. - function Code_Address_For_AAA return System.Address is - begin - -- We are using a label instead of Code_Address_For_AAA'Address because - -- on some platforms the latter does not yield the address we want, but - -- the address of a stub or of a descriptor instead. This is the case at - -- least on PA-HPUX. - - <<Start_Of_AAA>> - return Start_Of_AAA'Address; - end Code_Address_For_AAA; + procedure AAA is null; ---------------- -- Call_Chain -- @@ -1816,18 +1810,14 @@ package body Ada.Exceptions is return W (1 .. L); end Wide_Wide_Exception_Name; - -------------------------- - -- Code_Address_For_ZZZ -- - -------------------------- + --------- + -- ZZZ -- + --------- -- This function gives us the end of the PC range for addresses -- within the exception unit itself. We hope that gigi/gcc keeps all the -- procedures in their original order. - function Code_Address_For_ZZZ return System.Address is - begin - <<Start_Of_ZZZ>> - return Start_Of_ZZZ'Address; - end Code_Address_For_ZZZ; + procedure ZZZ is null; end Ada.Exceptions; diff --git a/gcc/ada/libgnat/a-nbnbig.ads b/gcc/ada/libgnat/a-nbnbig.ads index 3979f14..382a7b6 100644 --- a/gcc/ada/libgnat/a-nbnbig.ads +++ b/gcc/ada/libgnat/a-nbnbig.ads @@ -30,9 +30,9 @@ pragma Assertion_Policy (Ghost => Ignore); package Ada.Numerics.Big_Numbers.Big_Integers_Ghost with SPARK_Mode, Ghost, - Pure + Pure, + Always_Terminates is - pragma Annotate (GNATprove, Always_Return, Big_Integers_Ghost); type Big_Integer is private with Integer_Literal => From_Universal_Image; @@ -75,13 +75,13 @@ is with Dynamic_Predicate => (if Is_Valid (Big_Positive) then Big_Positive > To_Big_Integer (0)), - Predicate_Failure => (raise Constraint_Error); + 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); + Predicate_Failure => raise Constraint_Error; function In_Range (Arg : Valid_Big_Integer; Low, High : Big_Integer) return Boolean @@ -96,7 +96,7 @@ is Pre => In_Range (Arg, Low => To_Big_Integer (Integer'First), High => To_Big_Integer (Integer'Last)) - or else (raise Constraint_Error), + or else raise Constraint_Error, Global => null; generic @@ -112,7 +112,7 @@ is Pre => In_Range (Arg, Low => To_Big_Integer (Int'First), High => To_Big_Integer (Int'Last)) - or else (raise Constraint_Error), + or else raise Constraint_Error, Global => null; end Signed_Conversions; @@ -129,7 +129,7 @@ is Pre => In_Range (Arg, Low => To_Big_Integer (Int'First), High => To_Big_Integer (Int'Last)) - or else (raise Constraint_Error), + or else raise Constraint_Error, Global => null; end Unsigned_Conversions; @@ -207,7 +207,7 @@ is with Import, Pre => (L /= To_Big_Integer (0) and R /= To_Big_Integer (0)) - or else (raise Constraint_Error), + or else raise Constraint_Error, Global => null; private diff --git a/gcc/ada/libgnat/a-nbnbin.adb b/gcc/ada/libgnat/a-nbnbin.adb index edfd04e..090f408 100644 --- a/gcc/ada/libgnat/a-nbnbin.adb +++ b/gcc/ada/libgnat/a-nbnbin.adb @@ -160,7 +160,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is function To_Integer (Arg : Valid_Big_Integer) return Integer is begin - return Integer (From_Bignum (Get_Bignum (Arg))); + return Integer (Long_Long_Integer'(From_Bignum (Get_Bignum (Arg)))); end To_Integer; ------------------------ @@ -186,7 +186,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is function From_Big_Integer (Arg : Valid_Big_Integer) return Int is begin - return Int (From_Bignum (Get_Bignum (Arg))); + return Int (Long_Long_Long_Integer'(From_Bignum (Get_Bignum (Arg)))); end From_Big_Integer; end Signed_Conversions; @@ -214,7 +214,7 @@ package body Ada.Numerics.Big_Numbers.Big_Integers is function From_Big_Integer (Arg : Valid_Big_Integer) return Int is begin - return Int (From_Bignum (Get_Bignum (Arg))); + return Int (Unsigned_128'(From_Bignum (Get_Bignum (Arg)))); end From_Big_Integer; end Unsigned_Conversions; diff --git a/gcc/ada/libgnat/a-nbnbin.ads b/gcc/ada/libgnat/a-nbnbin.ads index ffb96d4..c4d74ee 100644 --- a/gcc/ada/libgnat/a-nbnbin.ads +++ b/gcc/ada/libgnat/a-nbnbin.ads @@ -18,10 +18,10 @@ with Ada.Strings.Text_Buffers; use Ada.Strings.Text_Buffers; private with Ada.Finalization; private with System; -package Ada.Numerics.Big_Numbers.Big_Integers - with Preelaborate +package Ada.Numerics.Big_Numbers.Big_Integers with + Preelaborate, + Always_Terminates is - pragma Annotate (GNATprove, Always_Return, Big_Integers); type Big_Integer is private with Integer_Literal => From_Universal_Image, diff --git a/gcc/ada/libgnat/a-nbnbre.ads b/gcc/ada/libgnat/a-nbnbre.ads index 350d049..d342eeb 100644 --- a/gcc/ada/libgnat/a-nbnbre.ads +++ b/gcc/ada/libgnat/a-nbnbre.ads @@ -17,10 +17,10 @@ with Ada.Numerics.Big_Numbers.Big_Integers; with Ada.Strings.Text_Buffers; use Ada.Strings.Text_Buffers; -package Ada.Numerics.Big_Numbers.Big_Reals - with Preelaborate +package Ada.Numerics.Big_Numbers.Big_Reals with + Preelaborate, + Always_Terminates is - pragma Annotate (GNATprove, Always_Return, Big_Reals); type Big_Real is private with Real_Literal => From_Universal_Image, diff --git a/gcc/ada/libgnat/a-ngelfu.ads b/gcc/ada/libgnat/a-ngelfu.ads index f6d6c96..444d1a3 100644 --- a/gcc/ada/libgnat/a-ngelfu.ads +++ b/gcc/ada/libgnat/a-ngelfu.ads @@ -37,10 +37,10 @@ generic type Float_Type is digits <>; package Ada.Numerics.Generic_Elementary_Functions with - SPARK_Mode => On + SPARK_Mode => On, + Always_Terminates is pragma Pure; - pragma Annotate (GNATprove, Always_Return, Generic_Elementary_Functions); -- Preconditions in this unit are meant for analysis only, not for run-time -- checking, so that the expected exceptions are raised when calling diff --git a/gcc/ada/libgnat/a-nlelfu.ads b/gcc/ada/libgnat/a-nlelfu.ads index b3afd1f..10b33e9 100644 --- a/gcc/ada/libgnat/a-nlelfu.ads +++ b/gcc/ada/libgnat/a-nlelfu.ads @@ -19,4 +19,3 @@ package Ada.Numerics.Long_Elementary_Functions is new Ada.Numerics.Generic_Elementary_Functions (Long_Float); pragma Pure (Long_Elementary_Functions); -pragma Annotate (GNATprove, Always_Return, Long_Elementary_Functions); diff --git a/gcc/ada/libgnat/a-nllefu.ads b/gcc/ada/libgnat/a-nllefu.ads index e137c67..7089fc3 100644 --- a/gcc/ada/libgnat/a-nllefu.ads +++ b/gcc/ada/libgnat/a-nllefu.ads @@ -19,4 +19,3 @@ package Ada.Numerics.Long_Long_Elementary_Functions is new Ada.Numerics.Generic_Elementary_Functions (Long_Long_Float); pragma Pure (Long_Long_Elementary_Functions); -pragma Annotate (GNATprove, Always_Return, Long_Long_Elementary_Functions); diff --git a/gcc/ada/libgnat/a-nselfu.ads b/gcc/ada/libgnat/a-nselfu.ads index 6797efd..10b04ac 100644 --- a/gcc/ada/libgnat/a-nselfu.ads +++ b/gcc/ada/libgnat/a-nselfu.ads @@ -19,4 +19,3 @@ package Ada.Numerics.Short_Elementary_Functions is new Ada.Numerics.Generic_Elementary_Functions (Short_Float); pragma Pure (Short_Elementary_Functions); -pragma Annotate (GNATprove, Always_Return, Short_Elementary_Functions); diff --git a/gcc/ada/libgnat/a-nuelfu.ads b/gcc/ada/libgnat/a-nuelfu.ads index d4fe745..149939b 100644 --- a/gcc/ada/libgnat/a-nuelfu.ads +++ b/gcc/ada/libgnat/a-nuelfu.ads @@ -19,4 +19,3 @@ package Ada.Numerics.Elementary_Functions is new Ada.Numerics.Generic_Elementary_Functions (Float); pragma Pure (Elementary_Functions); -pragma Annotate (GNATprove, Always_Return, Elementary_Functions); diff --git a/gcc/ada/libgnat/a-rbtgbo.adb b/gcc/ada/libgnat/a-rbtgbo.adb index 773e71a..2f96579 100644 --- a/gcc/ada/libgnat/a-rbtgbo.adb +++ b/gcc/ada/libgnat/a-rbtgbo.adb @@ -207,21 +207,21 @@ package body Ada.Containers.Red_Black_Trees.Generic_Bounded_Operations is pragma Assert (Tree.Last /= 0); pragma Assert (Parent (N (Tree.Root)) = 0); - pragma Assert ((Tree.Length > 1) + pragma Assert (Tree.Length > 1 or else (Tree.First = Tree.Last and then Tree.First = Tree.Root)); - pragma Assert ((Left (N (Node)) = 0) - or else (Parent (N (Left (N (Node)))) = Node)); + pragma Assert (Left (N (Node)) = 0 + or else Parent (N (Left (N (Node)))) = Node); - pragma Assert ((Right (N (Node)) = 0) - or else (Parent (N (Right (N (Node)))) = Node)); + pragma Assert (Right (N (Node)) = 0 + or else Parent (N (Right (N (Node)))) = Node); - pragma Assert (((Parent (N (Node)) = 0) and then (Tree.Root = Node)) - or else ((Parent (N (Node)) /= 0) and then - ((Left (N (Parent (N (Node)))) = Node) + pragma Assert ((Parent (N (Node)) = 0 and then Tree.Root = Node) + or else (Parent (N (Node)) /= 0 and then + (Left (N (Parent (N (Node)))) = Node or else - (Right (N (Parent (N (Node)))) = Node)))); + Right (N (Parent (N (Node)))) = Node))); if Left (N (Z)) = 0 then if Right (N (Z)) = 0 then diff --git a/gcc/ada/libgnat/a-strbou.ads b/gcc/ada/libgnat/a-strbou.ads index 0ada787..ea0cc3f 100644 --- a/gcc/ada/libgnat/a-strbou.ads +++ b/gcc/ada/libgnat/a-strbou.ads @@ -47,9 +47,11 @@ with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function; with Ada.Strings.Superbounded; with Ada.Strings.Search; -package Ada.Strings.Bounded with SPARK_Mode is +package Ada.Strings.Bounded with + SPARK_Mode, + Always_Terminates +is pragma Preelaborate; - pragma Annotate (GNATprove, Always_Return, Bounded); generic Max : Positive; @@ -57,7 +59,8 @@ package Ada.Strings.Bounded with SPARK_Mode is package Generic_Bounded_Length with SPARK_Mode, Initial_Condition => Length (Null_Bounded_String) = 0, - Abstract_State => null + Abstract_State => null, + Always_Terminates is -- Preconditions in this unit are meant for analysis only, not for -- run-time checking, so that the expected exceptions are raised. This @@ -69,7 +72,6 @@ package Ada.Strings.Bounded with SPARK_Mode is Post => Ignore, Contract_Cases => Ignore, Ghost => Ignore); - pragma Annotate (GNATprove, Always_Return, Generic_Bounded_Length); Max_Length : constant Positive := Max; @@ -1341,6 +1343,9 @@ package Ada.Strings.Bounded with SPARK_Mode is (for all K in 1 .. Length (Source) => Element (Translate'Result, K) = Mapping (Element (Source, K))), Global => null; + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); procedure Translate (Source : in out Bounded_String; @@ -1352,6 +1357,9 @@ package Ada.Strings.Bounded with SPARK_Mode is (for all K in 1 .. Length (Source) => Element (Source, K) = Mapping (Element (Source'Old, K))), Global => null; + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); --------------------------------------- -- String Transformation Subprograms -- diff --git a/gcc/ada/libgnat/a-strfix.adb b/gcc/ada/libgnat/a-strfix.adb index 7e8ac1c..ace705d 100644 --- a/gcc/ada/libgnat/a-strfix.adb +++ b/gcc/ada/libgnat/a-strfix.adb @@ -773,12 +773,18 @@ package body Ada.Strings.Fixed with SPARK_Mode is do for J in Source'Range loop Result (J - (Source'First - 1)) := Mapping.all (Source (J)); + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); pragma Loop_Invariant (for all K in Source'First .. J => Result (K - (Source'First - 1))'Initialized); pragma Loop_Invariant (for all K in Source'First .. J => Result (K - (Source'First - 1)) = Mapping (Source (K))); + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); end loop; end return; end Translate; @@ -791,9 +797,15 @@ package body Ada.Strings.Fixed with SPARK_Mode is begin for J in Source'Range loop Source (J) := Mapping.all (Source (J)); + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); pragma Loop_Invariant (for all K in Source'First .. J => Source (K) = Mapping (Source'Loop_Entry (K))); + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); end loop; end Translate; diff --git a/gcc/ada/libgnat/a-strfix.ads b/gcc/ada/libgnat/a-strfix.ads index dee64ab..9d5e9d9 100644 --- a/gcc/ada/libgnat/a-strfix.ads +++ b/gcc/ada/libgnat/a-strfix.ads @@ -46,7 +46,10 @@ pragma Assertion_Policy (Pre => Ignore, with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function; with Ada.Strings.Search; -package Ada.Strings.Fixed with SPARK_Mode is +package Ada.Strings.Fixed with + SPARK_Mode, + Always_Terminates +is pragma Preelaborate; -------------------------------------------------------------- @@ -60,11 +63,9 @@ package Ada.Strings.Fixed with SPARK_Mode is Justify : Alignment := Left; Pad : Character := Space) with - - -- Incomplete contract - - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => + (Length_Error => Target'Length'Old < Source'Length and Drop = Error); -- The Move procedure copies characters from Source to Target. If Source -- has the same length as Target, then the effect is to assign Source to -- Target. If Source is shorter than Target then: @@ -169,8 +170,7 @@ package Ada.Strings.Fixed with SPARK_Mode is others => Index'Result = 0), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; pragma Ada_05 (Index); function Index @@ -233,8 +233,7 @@ package Ada.Strings.Fixed with SPARK_Mode is others => Index'Result = 0), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; pragma Ada_05 (Index); -- Each Index function searches, starting from From, for a slice of @@ -303,8 +302,7 @@ package Ada.Strings.Fixed with SPARK_Mode is others => Index'Result = 0), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; function Index (Source : String; @@ -359,8 +357,7 @@ package Ada.Strings.Fixed with SPARK_Mode is others => Index'Result = 0), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; -- If Going = Forward, returns: -- @@ -413,8 +410,7 @@ package Ada.Strings.Fixed with SPARK_Mode is and then (J < Index'Result) = (Going = Forward) then (Test = Inside) /= Ada.Strings.Maps.Is_In (Source (J), Set)))), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; function Index (Source : String; @@ -470,8 +466,7 @@ package Ada.Strings.Fixed with SPARK_Mode is or else (J > From) = (Going = Forward)) then (Test = Inside) /= Ada.Strings.Maps.Is_In (Source (J), Set)))), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; pragma Ada_05 (Index); -- Index searches for the first or last occurrence of any of a set of -- characters (when Test=Inside), or any of the complement of a set of @@ -531,8 +526,7 @@ package Ada.Strings.Fixed with SPARK_Mode is and then (J = From or else (J > From) = (Going = Forward)) then Source (J) = ' '))), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; pragma Ada_05 (Index_Non_Blank); -- Returns Index (Source, Maps.To_Set(Space), From, Outside, Going) @@ -570,8 +564,7 @@ package Ada.Strings.Fixed with SPARK_Mode is and then (J < Index_Non_Blank'Result) = (Going = Forward) then Source (J) = ' '))), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; -- Returns Index (Source, Maps.To_Set(Space), Outside, Going) function Count @@ -579,18 +572,16 @@ package Ada.Strings.Fixed with SPARK_Mode is Pattern : String; Mapping : Maps.Character_Mapping := Maps.Identity) return Natural with - Pre => Pattern'Length /= 0, - Global => null, - Annotate => (GNATprove, Always_Return); + Pre => Pattern'Length /= 0, + Global => null; function Count (Source : String; Pattern : String; Mapping : Maps.Character_Mapping_Function) return Natural with - Pre => Pattern'Length /= 0 and then Mapping /= null, - Global => null, - Annotate => (GNATprove, Always_Return); + Pre => Pattern'Length /= 0 and then Mapping /= null, + Global => null; -- Returns the maximum number of nonoverlapping slices of Source that match -- Pattern with respect to Mapping. If Pattern is the null string then @@ -600,8 +591,7 @@ package Ada.Strings.Fixed with SPARK_Mode is (Source : String; Set : Maps.Character_Set) return Natural with - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; -- Returns the number of occurrences in Source of characters that are in -- Set. @@ -659,8 +649,7 @@ package Ada.Strings.Fixed with SPARK_Mode is then (Test = Inside) /= Ada.Strings.Maps.Is_In (Source (Last + 1), Set))), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; pragma Ada_2012 (Find_Token); -- If Source is not the null string and From is not in Source'Range, then -- Index_Error is raised. Otherwise, First is set to the index of the first @@ -722,8 +711,7 @@ package Ada.Strings.Fixed with SPARK_Mode is then (Test = Inside) /= Ada.Strings.Maps.Is_In (Source (Last + 1), Set))), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; -- Equivalent to Find_Token (Source, Set, Source'First, Test, First, Last) ------------------------------------ @@ -752,8 +740,10 @@ package Ada.Strings.Fixed with SPARK_Mode is (for all J in Source'Range => Translate'Result (J - Source'First + 1) = Mapping (Source (J))), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); function Translate (Source : String; @@ -776,8 +766,7 @@ package Ada.Strings.Fixed with SPARK_Mode is (for all J in Source'Range => Translate'Result (J - Source'First + 1) = Ada.Strings.Maps.Value (Mapping, Source (J))), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; -- Returns the string S whose length is Source'Length and such that S (I) -- is the character to which Mapping maps the corresponding element of @@ -787,29 +776,30 @@ package Ada.Strings.Fixed with SPARK_Mode is (Source : in out String; Mapping : Maps.Character_Mapping_Function) with - Pre => Mapping /= null, - Post => + Pre => Mapping /= null, + Post => -- Each character in Source after the call is the translation of the -- character at the same position before the call, through Mapping. (for all J in Source'Range => Source (J) = Mapping (Source'Old (J))), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); procedure Translate (Source : in out String; Mapping : Maps.Character_Mapping) with - Post => + Post => -- Each character in Source after the call is the translation of the -- character at the same position before the call, through Mapping. (for all J in Source'Range => Source (J) = Ada.Strings.Maps.Value (Mapping, Source'Old (J))), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; -- Equivalent to Source := Translate(Source, Mapping) @@ -902,8 +892,7 @@ package Ada.Strings.Fixed with SPARK_Mode is (Low - Source'First + By'Length + 1 .. Replace_Slice'Result'Last) = Source (Low .. Source'Last))), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; -- If Low > Source'Last + 1, or High < Source'First - 1, then Index_Error -- is propagated. Otherwise: -- @@ -923,7 +912,7 @@ package Ada.Strings.Fixed with SPARK_Mode is Justify : Alignment := Left; Pad : Character := Space) with - Pre => + Pre => Low - 1 <= Source'Last and then High >= Source'First - 1 and then (if High >= Low @@ -932,11 +921,8 @@ package Ada.Strings.Fixed with SPARK_Mode is - By'Length - Natural'Max (Source'Last - High, 0) else Source'Length <= Natural'Last - By'Length), - - -- Incomplete contract - - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => (Length_Error => Drop = Error); -- Equivalent to: -- -- Move (Replace_Slice (Source, Low, High, By), @@ -982,8 +968,7 @@ package Ada.Strings.Fixed with SPARK_Mode is (Before - Source'First + New_Item'Length + 1 .. Insert'Result'Last) = Source (Before .. Source'Last)), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; -- Propagates Index_Error if Before is not in -- Source'First .. Source'Last + 1; otherwise, returns -- Source (Source'First .. Before - 1) @@ -995,14 +980,11 @@ package Ada.Strings.Fixed with SPARK_Mode is New_Item : String; Drop : Truncation := Error) with - Pre => + Pre => Before - 1 in Source'First - 1 .. Source'Last and then Source'Length <= Natural'Last - New_Item'Length, - - -- Incomplete contract - - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => (Length_Error => Drop = Error); -- Equivalent to Move (Insert (Source, Before, New_Item), Source, Drop) function Overwrite @@ -1051,8 +1033,7 @@ package Ada.Strings.Fixed with SPARK_Mode is (Position - Source'First + New_Item'Length + 1 .. Overwrite'Result'Last) = Source (Position + New_Item'Length .. Source'Last)), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; -- Propagates Index_Error if Position is not in -- Source'First .. Source'Last + 1; otherwise, returns the string obtained -- from Source by consecutively replacing characters starting at Position @@ -1066,16 +1047,13 @@ package Ada.Strings.Fixed with SPARK_Mode is New_Item : String; Drop : Truncation := Right) with - Pre => + Pre => Position - 1 in Source'First - 1 .. Source'Last and then (if Position - Source'First >= Source'Length - New_Item'Length then Position - Source'First <= Natural'Last - New_Item'Length), - - -- Incomplete contract - - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => (Length_Error => Drop = Error); -- Equivalent to Move(Overwrite(Source, Position, New_Item), Source, Drop) function Delete @@ -1123,8 +1101,7 @@ package Ada.Strings.Fixed with SPARK_Mode is others => Delete'Result'Length = Source'Length and then Delete'Result = Source), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; -- If From <= Through, the returned string is -- Replace_Slice(Source, From, Through, ""); otherwise, it is Source with -- lower bound 1. @@ -1136,14 +1113,10 @@ package Ada.Strings.Fixed with SPARK_Mode is Justify : Alignment := Left; Pad : Character := Space) with - Pre => (if From <= Through + Pre => (if From <= Through then (From in Source'Range and then Through <= Source'Last)), - - -- Incomplete contract - - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null; -- Equivalent to: -- -- Move (Delete (Source, From, Through), @@ -1157,7 +1130,7 @@ package Ada.Strings.Fixed with SPARK_Mode is (Source : String; Side : Trim_End) return String with - Post => + Post => -- Lower bound of the returned string is 1 @@ -1182,8 +1155,7 @@ package Ada.Strings.Fixed with SPARK_Mode is else Index_Non_Blank (Source, Backward)); begin Trim'Result = Source (Low .. High))), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; -- Returns the string obtained by removing from Source all leading Space -- characters (if Side = Left), all trailing Space characters (if -- Side = Right), or all leading and trailing Space characters (if @@ -1195,11 +1167,7 @@ package Ada.Strings.Fixed with SPARK_Mode is Justify : Alignment := Left; Pad : Character := Space) with - - -- Incomplete contract - - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null; -- Equivalent to: -- -- Move (Trim (Source, Side), Source, Justify=>Justify, Pad=>Pad). @@ -1236,8 +1204,7 @@ package Ada.Strings.Fixed with SPARK_Mode is Index (Source, Right, Outside, Backward); begin Trim'Result = Source (Low .. High))), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; -- Returns the string obtained by removing from Source all leading -- characters in Left and all trailing characters in Right. @@ -1248,11 +1215,7 @@ package Ada.Strings.Fixed with SPARK_Mode is Justify : Alignment := Strings.Left; Pad : Character := Space) with - - -- Incomplete contract - - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null; -- Equivalent to: -- -- Move (Trim (Source, Left, Right), @@ -1289,8 +1252,7 @@ package Ada.Strings.Fixed with SPARK_Mode is and then Head'Result (Source'Length + 1 .. Count) = [1 .. Count - Source'Length => Pad]), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; -- Returns a string of length Count. If Count <= Source'Length, the string -- comprises the first Count characters of Source. Otherwise, its contents -- are Source concatenated with Count - Source'Length Pad characters. @@ -1301,11 +1263,8 @@ package Ada.Strings.Fixed with SPARK_Mode is Justify : Alignment := Left; Pad : Character := Space) with - - -- Incomplete contract - - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => (Length_Error => Count > Source'Length'Old); -- Equivalent to: -- -- Move (Head (Source, Count, Pad), @@ -1354,8 +1313,7 @@ package Ada.Strings.Fixed with SPARK_Mode is and then Tail'Result (Count - Source'Length + 1 .. Tail'Result'Last) = Source)), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; -- Returns a string of length Count. If Count <= Source'Length, the string -- comprises the last Count characters of Source. Otherwise, its contents -- are Count-Source'Length Pad characters concatenated with Source. @@ -1366,11 +1324,8 @@ package Ada.Strings.Fixed with SPARK_Mode is Justify : Alignment := Left; Pad : Character := Space) with - - -- Incomplete contract - - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => (Length_Error => Count > Source'Length'Old); -- Equivalent to: -- -- Move (Tail (Source, Count, Pad), @@ -1384,7 +1339,7 @@ package Ada.Strings.Fixed with SPARK_Mode is (Left : Natural; Right : Character) return String with - Post => + Post => -- Lower bound of the returned string is 1 @@ -1397,8 +1352,7 @@ package Ada.Strings.Fixed with SPARK_Mode is -- All characters of the returned string are Right and then (for all C of "*"'Result => C = Right), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; function "*" (Left : Natural; @@ -1421,8 +1375,7 @@ package Ada.Strings.Fixed with SPARK_Mode is and then (for all K in "*"'Result'Range => "*"'Result (K) = Right (Right'First + (K - 1) mod Right'Length)), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; -- These functions replicate a character or string a specified number of -- times. The first function returns a string whose length is Left and each diff --git a/gcc/ada/libgnat/a-strmap.adb b/gcc/ada/libgnat/a-strmap.adb index 53af28b..529ecbb 100644 --- a/gcc/ada/libgnat/a-strmap.adb +++ b/gcc/ada/libgnat/a-strmap.adb @@ -545,7 +545,7 @@ is Result (Char) = ((for some Prev in Ranges'First .. R - 1 => Char in Ranges (Prev).Low .. Ranges (Prev).High) - or else (Char in Ranges (R).Low .. C))); + or else Char in Ranges (R).Low .. C)); end loop; pragma Loop_Invariant diff --git a/gcc/ada/libgnat/a-strmap.ads b/gcc/ada/libgnat/a-strmap.ads index 73dd3d9..a070da0 100644 --- a/gcc/ada/libgnat/a-strmap.ads +++ b/gcc/ada/libgnat/a-strmap.ads @@ -48,14 +48,13 @@ pragma Assertion_Policy (Pre => Ignore, with Ada.Characters.Latin_1; -package Ada.Strings.Maps - with SPARK_Mode +package Ada.Strings.Maps with + SPARK_Mode, + Always_Terminates is pragma Pure; -- In accordance with Ada 2005 AI-362 - pragma Annotate (GNATprove, Always_Return, Maps); - -------------------------------- -- Character Set Declarations -- -------------------------------- diff --git a/gcc/ada/libgnat/a-strsea.adb b/gcc/ada/libgnat/a-strsea.adb index ef35843..614b5ac 100644 --- a/gcc/ada/libgnat/a-strsea.adb +++ b/gcc/ada/libgnat/a-strsea.adb @@ -185,6 +185,9 @@ package body Ada.Strings.Search with SPARK_Mode is Ind := Ind + 1; for K in Pattern'Range loop if Pattern (K) /= Mapping (Source (Ind + (K - Pattern'First))) then + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); pragma Assert (not (Match (Source, Pattern, Mapping, Ind))); goto Cont; end if; @@ -192,6 +195,9 @@ package body Ada.Strings.Search with SPARK_Mode is pragma Loop_Invariant (for all J in Pattern'First .. K => Pattern (J) = Mapping (Source (Ind + (J - Pattern'First)))); + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); end loop; pragma Assert (Match (Source, Pattern, Mapping, Ind)); @@ -489,12 +495,18 @@ package body Ada.Strings.Search with SPARK_Mode is if Pattern (K) /= Mapping.all (Source (Ind + (K - Pattern'First))) then + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); goto Cont1; end if; pragma Loop_Invariant (for all J in Pattern'First .. K => Pattern (J) = Mapping (Source (Ind + (J - Pattern'First)))); + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); end loop; pragma Assert (Match (Source, Pattern, Mapping, Ind)); @@ -515,19 +527,25 @@ package body Ada.Strings.Search with SPARK_Mode is if Pattern (K) /= Mapping.all (Source (Ind + (K - Pattern'First))) then + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); goto Cont2; end if; pragma Loop_Invariant (for all J in Pattern'First .. K => Pattern (J) = Mapping (Source (Ind + (J - Pattern'First)))); + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); end loop; return Ind; <<Cont2>> pragma Loop_Invariant - (for all J in Ind .. (Source'Last - PL1) => + (for all J in Ind .. Source'Last - PL1 => not (Match (Source, Pattern, Mapping, J))); null; end loop; diff --git a/gcc/ada/libgnat/a-strsea.ads b/gcc/ada/libgnat/a-strsea.ads index 2c24e1a..df1b342 100644 --- a/gcc/ada/libgnat/a-strsea.ads +++ b/gcc/ada/libgnat/a-strsea.ads @@ -50,9 +50,11 @@ pragma Assertion_Policy (Pre => Ignore, with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function; -package Ada.Strings.Search with SPARK_Mode is +package Ada.Strings.Search with + SPARK_Mode, + Always_Terminates +is pragma Preelaborate; - pragma Annotate (GNATprove, Always_Return, Search); -- The ghost function Match tells whether the slice of Source starting at -- From and of length Pattern'Length matches with Pattern with respect to @@ -74,6 +76,9 @@ package Ada.Strings.Search with SPARK_Mode is and then Source'Length > 0 and then From in Source'First .. Source'Last - (Pattern'Length - 1), Global => null; + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); function Match (Source : String; diff --git a/gcc/ada/libgnat/a-strsup.adb b/gcc/ada/libgnat/a-strsup.adb index a9323cf..c727575 100644 --- a/gcc/ada/libgnat/a-strsup.adb +++ b/gcc/ada/libgnat/a-strsup.adb @@ -29,12 +29,13 @@ -- -- ------------------------------------------------------------------------------ --- Ghost code, loop invariants and assertions in this unit are meant for +-- Ghost code, loop (in)variants 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, + Loop_Variant => Ignore, Assert => Ignore); with Ada.Strings.Maps; use Ada.Strings.Maps; @@ -1570,6 +1571,7 @@ package body Ada.Strings.Superbounded with SPARK_Mode is (for all K in 1 .. Indx => Result.Data (K) = Item (Item'First + (K - 1) mod Ilen)); + pragma Loop_Variant (Increases => Indx); end loop; Result.Data (Indx + 1 .. Max_Length) := Super_String_Data @@ -1609,6 +1611,7 @@ package body Ada.Strings.Superbounded with SPARK_Mode is (for all K in Indx + 1 .. Max_Length => Result.Data (K) = Item (Item'Last - (Max_Length - K) mod Ilen)); + pragma Loop_Variant (Decreases => Indx); end loop; Result.Data (1 .. Indx) := @@ -1654,6 +1657,7 @@ package body Ada.Strings.Superbounded with SPARK_Mode is Low : Positive; High : Natural) return Super_String is + Len : constant Natural := (if Low > High then 0 else High - Low + 1); begin return Result : Super_String (Source.Max_Length) do if Low - 1 > Source.Current_Length @@ -1662,9 +1666,8 @@ package body Ada.Strings.Superbounded with SPARK_Mode is raise Index_Error; end if; - Result.Current_Length := (if Low > High then 0 else High - Low + 1); - Result.Data (1 .. Result.Current_Length) := - Source.Data (Low .. High); + Result.Data (1 .. Len) := Source.Data (Low .. High); + Result.Current_Length := Len; end return; end Super_Slice; @@ -1674,6 +1677,7 @@ package body Ada.Strings.Superbounded with SPARK_Mode is Low : Positive; High : Natural) is + Len : constant Natural := (if Low > High then 0 else High - Low + 1); begin if Low - 1 > Source.Current_Length or else High > Source.Current_Length @@ -1681,8 +1685,8 @@ package body Ada.Strings.Superbounded with SPARK_Mode is raise Index_Error; end if; - Target.Current_Length := (if Low > High then 0 else High - Low + 1); - Target.Data (1 .. Target.Current_Length) := Source.Data (Low .. High); + Target.Data (1 .. Len) := Source.Data (Low .. High); + Target.Current_Length := Len; end Super_Slice; ---------------- @@ -1784,6 +1788,12 @@ package body Ada.Strings.Superbounded with SPARK_Mode is Source.Data (1 .. Npad) := [others => Pad]; Source.Data (Npad + 1 .. Max_Length) := Temp (1 .. Max_Length - Npad); + + pragma Assert + (Source.Data (1 .. Npad) = [1 .. Npad => Pad]); + pragma Assert + (Source.Data (Npad + 1 .. Max_Length) + = Temp (1 .. Max_Length - Npad)); end if; when Strings.Left => @@ -1844,10 +1854,16 @@ package body Ada.Strings.Superbounded with SPARK_Mode is begin for J in 1 .. Source.Current_Length loop Result.Data (J) := Mapping.all (Source.Data (J)); + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); pragma Loop_Invariant (Result.Data (1 .. J)'Initialized); pragma Loop_Invariant (for all K in 1 .. J => Result.Data (K) = Mapping (Source.Data (K))); + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); end loop; Result.Current_Length := Source.Current_Length; @@ -1861,9 +1877,15 @@ package body Ada.Strings.Superbounded with SPARK_Mode is begin for J in 1 .. Source.Current_Length loop Source.Data (J) := Mapping.all (Source.Data (J)); + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); pragma Loop_Invariant (for all K in 1 .. J => Source.Data (K) = Mapping (Source'Loop_Entry.Data (K))); + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); end loop; end Super_Translate; diff --git a/gcc/ada/libgnat/a-strsup.ads b/gcc/ada/libgnat/a-strsup.ads index 14e78e4..339cb17 100644 --- a/gcc/ada/libgnat/a-strsup.ads +++ b/gcc/ada/libgnat/a-strsup.ads @@ -51,7 +51,10 @@ with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function; with Ada.Strings.Search; with Ada.Strings.Text_Buffers; -package Ada.Strings.Superbounded with SPARK_Mode is +package Ada.Strings.Superbounded with + SPARK_Mode, + Always_Terminates +is pragma Preelaborate; -- Type Bounded_String in Ada.Strings.Bounded.Generic_Bounded_Length is @@ -68,7 +71,7 @@ package Ada.Strings.Superbounded with SPARK_Mode is -- Leaving it out is more efficient. end record with - Predicate => + Ghost_Predicate => Current_Length <= Max_Length and then Data (1 .. Current_Length)'Initialized, Put_Image => Put_Image; @@ -1406,6 +1409,9 @@ package Ada.Strings.Superbounded with SPARK_Mode is Super_Element (Super_Translate'Result, K) = Mapping (Super_Element (Source, K))), Global => null; + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); procedure Super_Translate (Source : in out Super_String; @@ -1418,6 +1424,9 @@ package Ada.Strings.Superbounded with SPARK_Mode is Super_Element (Source, K) = Mapping (Super_Element (Source'Old, K))), Global => null; + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); --------------------------------------- -- String Transformation Subprograms -- diff --git a/gcc/ada/libgnat/a-strunb.ads b/gcc/ada/libgnat/a-strunb.ads index 0b0085a..be76ad2 100644 --- a/gcc/ada/libgnat/a-strunb.ads +++ b/gcc/ada/libgnat/a-strunb.ads @@ -54,10 +54,10 @@ private with Ada.Strings.Text_Buffers; package Ada.Strings.Unbounded with SPARK_Mode, - Initial_Condition => Length (Null_Unbounded_String) = 0 + Initial_Condition => Length (Null_Unbounded_String) = 0, + Always_Terminates is pragma Preelaborate; - pragma Annotate (GNATprove, Always_Return, Unbounded); type Unbounded_String is private with Default_Initial_Condition => Length (Unbounded_String) = 0; @@ -86,21 +86,22 @@ is function To_Unbounded_String (Source : String) return Unbounded_String with - Post => Length (To_Unbounded_String'Result) = Source'Length, + Post => To_String (To_Unbounded_String'Result) = Source, Global => null; -- Returns an Unbounded_String that represents Source function To_Unbounded_String (Length : Natural) return Unbounded_String with - Post => - Ada.Strings.Unbounded.Length (To_Unbounded_String'Result) = Length, - Global => null; + SPARK_Mode => Off, + Global => null; -- Returns an Unbounded_String that represents an uninitialized String -- whose length is Length. function To_String (Source : Unbounded_String) return String with - Post => To_String'Result'Length = Length (Source), + Post => + To_String'Result'First = 1 + and then To_String'Result'Length = Length (Source), Global => null; -- Returns the String with lower bound 1 represented by Source @@ -115,6 +116,7 @@ is (Target : out Unbounded_String; Source : String) with + Post => To_String (Target) = Source, Global => null; pragma Ada_05 (Set_Unbounded_String); -- Sets Target to an Unbounded_String that represents Source @@ -198,6 +200,7 @@ is Index : Positive) return Character with Pre => Index <= Length (Source), + Post => Element'Result = To_String (Source) (Index), Global => null; -- Returns the character at position Index in the string represented by -- Source; propagates Index_Error if Index > Length (Source). @@ -259,18 +262,21 @@ is (Left : Unbounded_String; Right : Unbounded_String) return Boolean with + Post => "="'Result = (To_String (Left) = To_String (Right)), Global => null; function "=" (Left : Unbounded_String; Right : String) return Boolean with + Post => "="'Result = (To_String (Left) = Right), Global => null; function "=" (Left : String; Right : Unbounded_String) return Boolean with + Post => "="'Result = (Left = To_String (Right)), Global => null; function "<" diff --git a/gcc/ada/libgnat/a-strunb__shared.ads b/gcc/ada/libgnat/a-strunb__shared.ads index bb69056..2da9dc7 100644 --- a/gcc/ada/libgnat/a-strunb__shared.ads +++ b/gcc/ada/libgnat/a-strunb__shared.ads @@ -83,10 +83,10 @@ private with System.Atomic_Counters; private with Ada.Strings.Text_Buffers; package Ada.Strings.Unbounded with - Initial_Condition => Length (Null_Unbounded_String) = 0 + Initial_Condition => Length (Null_Unbounded_String) = 0, + Always_Terminates is pragma Preelaborate; - pragma Annotate (GNATprove, Always_Return, Unbounded); type Unbounded_String is private with Default_Initial_Condition => Length (Unbounded_String) = 0; @@ -108,24 +108,26 @@ is function To_Unbounded_String (Source : String) return Unbounded_String with - Post => Length (To_Unbounded_String'Result) = Source'Length, + Post => To_String (To_Unbounded_String'Result) = Source, Global => null; function To_Unbounded_String (Length : Natural) return Unbounded_String with - Post => - Ada.Strings.Unbounded.Length (To_Unbounded_String'Result) = Length, - Global => null; + SPARK_Mode => Off, + Global => null; function To_String (Source : Unbounded_String) return String with - Post => To_String'Result'Length = Length (Source), + Post => + To_String'Result'First = 1 + and then To_String'Result'Length = Length (Source), Global => null; procedure Set_Unbounded_String (Target : out Unbounded_String; Source : String) with + Post => To_String (Target) = Source, Global => null; pragma Ada_05 (Set_Unbounded_String); @@ -198,6 +200,7 @@ is Index : Positive) return Character with Pre => Index <= Length (Source), + Post => Element'Result = To_String (Source) (Index), Global => null; procedure Replace_Element @@ -244,18 +247,21 @@ is (Left : Unbounded_String; Right : Unbounded_String) return Boolean with + Post => "="'Result = (To_String (Left) = To_String (Right)), Global => null; function "=" (Left : Unbounded_String; Right : String) return Boolean with + Post => "="'Result = (To_String (Left) = Right), Global => null; function "=" (Left : String; Right : Unbounded_String) return Boolean with + Post => "="'Result = (Left = To_String (Right)), Global => null; function "<" diff --git a/gcc/ada/libgnat/a-ststio.adb b/gcc/ada/libgnat/a-ststio.adb index fd1017f..ab46f48 100644 --- a/gcc/ada/libgnat/a-ststio.adb +++ b/gcc/ada/libgnat/a-ststio.adb @@ -354,7 +354,7 @@ package body Ada.Streams.Stream_IO is -- mode now. Note that we can use Inout_File as the mode for the -- call since File_IO handles all modes for all file types. - if ((File.Mode = FCB.In_File) /= (Mode = In_File)) + if (File.Mode = FCB.In_File) /= (Mode = In_File) and then not File.Update_Mode then FIO.Reset (AP (File)'Unrestricted_Access, FCB.Inout_File); @@ -367,11 +367,13 @@ package body Ada.Streams.Stream_IO is FIO.Append_Set (AP (File)); if File.Mode = FCB.Append_File then - if Standard'Address_Size = 64 then + pragma Warnings (Off, "condition is always *"); + if Memory_Size = 2**64 then File.Index := Count (ftell64 (File.Stream)) + 1; else File.Index := Count (ftell (File.Stream)) + 1; end if; + pragma Warnings (On); end if; File.Last_Op := Op_Other; diff --git a/gcc/ada/libgnat/a-suenco.adb b/gcc/ada/libgnat/a-suenco.adb index b3748f7..39a44bf 100644 --- a/gcc/ada/libgnat/a-suenco.adb +++ b/gcc/ada/libgnat/a-suenco.adb @@ -391,7 +391,7 @@ package body Ada.Strings.UTF_Encoding.Conversions is Result (Len + 1) := Character'Val - (2#11110_000# or (Shift_Right (zzzzz, 2))); + (2#11110_000# or Shift_Right (zzzzz, 2)); Result (Len + 2) := Character'Val (2#10_000000# or Shift_Left (zzzzz and 2#11#, 4) diff --git a/gcc/ada/libgnat/a-textio.ads b/gcc/ada/libgnat/a-textio.ads index 713116e..ddbbd85 100644 --- a/gcc/ada/libgnat/a-textio.ads +++ b/gcc/ada/libgnat/a-textio.ads @@ -59,7 +59,8 @@ package Ada.Text_IO with SPARK_Mode, Abstract_State => File_System, Initializes => File_System, - Initial_Condition => Line_Length = 0 and Page_Length = 0 + Initial_Condition => Line_Length = 0 and Page_Length = 0, + Always_Terminates is pragma Elaborate_Body; @@ -101,15 +102,15 @@ is Name : String := ""; Form : String := "") with - Pre => not Is_Open (File), - Post => + Pre => not Is_Open (File), + Post => Is_Open (File) and then Ada.Text_IO.Mode (File) = Mode and then (if Mode /= In_File then (Line_Length (File) = 0 and then Page_Length (File) = 0)), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Name_Error | Use_Error => Standard.True); procedure Open (File : in out File_Type; @@ -117,63 +118,63 @@ is Name : String; Form : String := "") with - Pre => not Is_Open (File), - Post => + Pre => not Is_Open (File), + Post => Is_Open (File) and then Ada.Text_IO.Mode (File) = Mode and then (if Mode /= In_File then (Line_Length (File) = 0 and then Page_Length (File) = 0)), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Name_Error | Use_Error => Standard.True); procedure Close (File : in out File_Type) with - Pre => Is_Open (File), - Post => not Is_Open (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + Pre => Is_Open (File), + Post => not Is_Open (File), + Global => (In_Out => File_System); + procedure Delete (File : in out File_Type) with - Pre => Is_Open (File), - Post => not Is_Open (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File), + Post => not Is_Open (File), + Global => (In_Out => File_System), + Exceptional_Cases => (Use_Error => Standard.True); + procedure Reset (File : in out File_Type; Mode : File_Mode) with - Pre => Is_Open (File), - Post => + Pre => Is_Open (File), + Post => Is_Open (File) and then Ada.Text_IO.Mode (File) = Mode and then (if Mode /= In_File then (Line_Length (File) = 0 and then Page_Length (File) = 0)), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Use_Error => Standard.True); + procedure Reset (File : in out File_Type) with - Pre => Is_Open (File), - Post => + Pre => Is_Open (File), + Post => Is_Open (File) and Mode (File)'Old = Mode (File) and (if Mode (File) /= In_File then (Line_Length (File) = 0 and then Page_Length (File) = 0)), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Use_Error => Standard.True); function Mode (File : File_Type) return File_Mode with - Pre => Is_Open (File), - Global => null, - Annotate => (GNATprove, Always_Return); + Pre => Is_Open (File), + Global => null; + function Name (File : File_Type) return String with - Pre => Is_Open (File), - Global => null, - Annotate => (GNATprove, Always_Return); + Pre => Is_Open (File), + SPARK_Mode => Off; + function Form (File : File_Type) return String with - Pre => Is_Open (File), - Global => null, - Annotate => (GNATprove, Always_Return); + Pre => Is_Open (File), + Global => null; function Is_Open (File : File_Type) return Boolean with - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; ------------------------------------------------------ -- Control of default input, output and error files -- @@ -209,342 +210,337 @@ is -- an oversight, and was intended to be IN, see AI95-00057. procedure Flush (File : File_Type) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => Line_Length (File)'Old = Line_Length (File) and Page_Length (File)'Old = Page_Length (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); + procedure Flush with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); -------------------------------------------- -- Specification of line and page lengths -- -------------------------------------------- procedure Set_Line_Length (File : File_Type; To : Count) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => Line_Length (File) = To and Page_Length (File)'Old = Page_Length (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Use_Error => Standard.True); + procedure Set_Line_Length (To : Count) with - Post => + Post => Line_Length = To and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Use_Error => Standard.True); procedure Set_Page_Length (File : File_Type; To : Count) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => Page_Length (File) = To and Line_Length (File)'Old = Line_Length (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Use_Error => Standard.True); + procedure Set_Page_Length (To : Count) with - Post => + Post => Page_Length = To and Line_Length'Old = Line_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Use_Error => Standard.True); function Line_Length (File : File_Type) return Count with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Global => (Input => File_System); + Pre => Is_Open (File) and then Mode (File) /= In_File, + Global => (Input => File_System); + function Line_Length return Count with - Global => (Input => File_System), - Annotate => (GNATprove, Always_Return); + Global => (Input => File_System); function Page_Length (File : File_Type) return Count with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Global => (Input => File_System); + Pre => Is_Open (File) and then Mode (File) /= In_File, + Global => (Input => File_System); + function Page_Length return Count with - Global => (Input => File_System), - Annotate => (GNATprove, Always_Return); + Global => (Input => File_System); ------------------------------------ -- Column, Line, and Page Control -- ------------------------------------ procedure New_Line (File : File_Type; Spacing : Positive_Count := 1) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => Line_Length (File)'Old = Line_Length (File) and Page_Length (File)'Old = Page_Length (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); + procedure New_Line (Spacing : Positive_Count := 1) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); procedure Skip_Line (File : File_Type; Spacing : Positive_Count := 1) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); + procedure Skip_Line (Spacing : Positive_Count := 1) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); function End_Of_Line (File : File_Type) return Boolean with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (Input => File_System), - Annotate => (GNATprove, Always_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (Input => File_System); + function End_Of_Line return Boolean with - Global => (Input => File_System), - Annotate => (GNATprove, Always_Return); + Global => (Input => File_System); procedure New_Page (File : File_Type) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => Line_Length (File)'Old = Line_Length (File) and Page_Length (File)'Old = Page_Length (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); + procedure New_Page with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); procedure Skip_Page (File : File_Type) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); + procedure Skip_Page with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); function End_Of_Page (File : File_Type) return Boolean with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (Input => File_System), - Annotate => (GNATprove, Always_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (Input => File_System); + function End_Of_Page return Boolean with - Global => (Input => File_System), - Annotate => (GNATprove, Always_Return); + Global => (Input => File_System); function End_Of_File (File : File_Type) return Boolean with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (Input => File_System), - Annotate => (GNATprove, Always_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (Input => File_System); + function End_Of_File return Boolean with - Global => (Input => File_System), - Annotate => (GNATprove, Always_Return); + Global => (Input => File_System); procedure Set_Col (File : File_Type; To : Positive_Count) with - Pre => + Pre => Is_Open (File) and then (if Mode (File) /= In_File then (Line_Length (File) = 0 or else To <= Line_Length (File))), - Contract_Cases => + Contract_Cases => (Mode (File) /= In_File => Line_Length (File)'Old = Line_Length (File) and Page_Length (File)'Old = Page_Length (File), others => True), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); + procedure Set_Col (To : Positive_Count) with - Pre => Line_Length = 0 or To <= Line_Length, - Post => + Pre => Line_Length = 0 or To <= Line_Length, + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); procedure Set_Line (File : File_Type; To : Positive_Count) with - Pre => + Pre => Is_Open (File) and then (if Mode (File) /= In_File then (Page_Length (File) = 0 or else To <= Page_Length (File))), - Contract_Cases => + Contract_Cases => (Mode (File) /= In_File => Line_Length (File)'Old = Line_Length (File) and Page_Length (File)'Old = Page_Length (File), others => True), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); + procedure Set_Line (To : Positive_Count) with - Pre => Page_Length = 0 or To <= Page_Length, - Post => + Pre => Page_Length = 0 or To <= Page_Length, + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); function Col (File : File_Type) return Positive_Count with - Pre => Is_Open (File), - Global => (Input => File_System), - Annotate => (GNATprove, Always_Return); + SPARK_Mode => Off; + function Col return Positive_Count with - Global => (Input => File_System), - Annotate => (GNATprove, Always_Return); + SPARK_Mode => Off; function Line (File : File_Type) return Positive_Count with - Pre => Is_Open (File), - Global => (Input => File_System), - Annotate => (GNATprove, Always_Return); + SPARK_Mode => Off; + function Line return Positive_Count with - Global => (Input => File_System), - Annotate => (GNATprove, Always_Return); + SPARK_Mode => Off; function Page (File : File_Type) return Positive_Count with - Pre => Is_Open (File), - Global => (Input => File_System), - Annotate => (GNATprove, Always_Return); + SPARK_Mode => Off; + function Page return Positive_Count with - Global => (Input => File_System), - Annotate => (GNATprove, Always_Return); + SPARK_Mode => Off; ---------------------------- -- Character Input-Output -- ---------------------------- procedure Get (File : File_Type; Item : out Character) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); + procedure Get (Item : out Character) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); + procedure Put (File : File_Type; Item : Character) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => Line_Length (File)'Old = Line_Length (File) and Page_Length (File)'Old = Page_Length (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); + procedure Put (Item : Character) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); procedure Look_Ahead (File : File_Type; Item : out Character; End_Of_Line : out Boolean) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (Input => File_System), - Annotate => (GNATprove, Always_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (Input => File_System); procedure Look_Ahead (Item : out Character; End_Of_Line : out Boolean) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (Input => File_System), - Annotate => (GNATprove, Always_Return); + Global => (Input => File_System); procedure Get_Immediate (File : File_Type; Item : out Character) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); procedure Get_Immediate (Item : out Character) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); procedure Get_Immediate (File : File_Type; Item : out Character; Available : out Boolean) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); procedure Get_Immediate (Item : out Character; Available : out Boolean) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); ------------------------- -- String Input-Output -- ------------------------- procedure Get (File : File_Type; Item : out String) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Item'Length'Old > 0); + procedure Get (Item : out String) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Item'Length'Old > 0); + procedure Put (File : File_Type; Item : String) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => Line_Length (File)'Old = Line_Length (File) and Page_Length (File)'Old = Page_Length (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); + procedure Put (Item : String) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); procedure Get_Line (File : File_Type; Item : out String; Last : out Natural) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Post => (if Item'Length > 0 then Last in Item'First - 1 .. Item'Last - else Last = Item'First - 1), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Post => + (if Item'Length > 0 then Last in Item'First - 1 .. Item'Last + else Last = Item'First - 1), + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Item'Length'Old > 0); procedure Get_Line (Item : out String; Last : out Natural) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length and (if Item'Length > 0 then Last in Item'First - 1 .. Item'Last else Last = Item'First - 1), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Item'Length'Old > 0); function Get_Line (File : File_Type) return String with SPARK_Mode => Off; pragma Ada_05 (Get_Line); @@ -556,21 +552,19 @@ is (File : File_Type; Item : String) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => Line_Length (File)'Old = Line_Length (File) and Page_Length (File)'Old = Page_Length (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); procedure Put_Line (Item : String) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); --------------------------------------- -- Generic packages for Input-Output -- diff --git a/gcc/ada/libgnat/a-tideio.ads b/gcc/ada/libgnat/a-tideio.ads index b62d251..7f8fa19 100644 --- a/gcc/ada/libgnat/a-tideio.ads +++ b/gcc/ada/libgnat/a-tideio.ads @@ -43,7 +43,9 @@ private generic type Num is delta <> digits <>; -package Ada.Text_IO.Decimal_IO is +package Ada.Text_IO.Decimal_IO with + Always_Terminates +is Default_Fore : Field := Num'Fore; Default_Aft : Field := Num'Aft; @@ -54,19 +56,19 @@ package Ada.Text_IO.Decimal_IO is Item : out Num; Width : Field := 0) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Exceptional_Cases => (Data_Error | End_Error => Standard.True); procedure Get (Item : out Num; Width : Field := 0) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Data_Error | End_Error => Standard.True); procedure Put (File : File_Type; @@ -75,12 +77,12 @@ package Ada.Text_IO.Decimal_IO is Aft : Field := Default_Aft; Exp : Field := Default_Exp) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => Line_Length (File)'Old = Line_Length (File) and Page_Length (File)'Old = Page_Length (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Layout_Error => Line_Length (File) /= 0); procedure Put (Item : Num; @@ -88,11 +90,11 @@ package Ada.Text_IO.Decimal_IO is Aft : Field := Default_Aft; Exp : Field := Default_Exp) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Layout_Error => Ada.Text_IO.Line_Length /= 0); procedure Get (From : String; @@ -100,7 +102,7 @@ package Ada.Text_IO.Decimal_IO is Last : out Positive) with Global => null, - Annotate => (GNATprove, Might_Not_Return); + Exceptional_Cases => (Data_Error => Standard.True); procedure Put (To : out String; @@ -108,8 +110,8 @@ package Ada.Text_IO.Decimal_IO is Aft : Field := Default_Aft; Exp : Field := Default_Exp) with - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => (Layout_Error => Standard.True); private pragma Inline (Get); diff --git a/gcc/ada/libgnat/a-tienio.ads b/gcc/ada/libgnat/a-tienio.ads index aac90f7..e4cdaee 100644 --- a/gcc/ada/libgnat/a-tienio.ads +++ b/gcc/ada/libgnat/a-tienio.ads @@ -23,21 +23,24 @@ private generic type Enum is (<>); -package Ada.Text_IO.Enumeration_IO is +package Ada.Text_IO.Enumeration_IO with + Always_Terminates +is Default_Width : Field := 0; Default_Setting : Type_Set := Upper_Case; procedure Get (File : File_Type; Item : out Enum) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Exceptional_Cases => (Data_Error | End_Error => Standard.True); + procedure Get (Item : out Enum) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Data_Error | End_Error => Standard.True); procedure Put (File : File_Type; @@ -45,38 +48,38 @@ package Ada.Text_IO.Enumeration_IO is Width : Field := Default_Width; Set : Type_Set := Default_Setting) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => Line_Length (File)'Old = Line_Length (File) and Page_Length (File)'Old = Page_Length (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Layout_Error => Line_Length (File) /= 0); procedure Put (Item : Enum; Width : Field := Default_Width; Set : Type_Set := Default_Setting) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Layout_Error => Ada.Text_IO.Line_Length /= 0); procedure Get (From : String; Item : out Enum; Last : out Positive) with - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => (Data_Error => Standard.True); procedure Put (To : out String; Item : Enum; Set : Type_Set := Default_Setting) with - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => (Layout_Error => Standard.True); end Ada.Text_IO.Enumeration_IO; diff --git a/gcc/ada/libgnat/a-tifiio.ads b/gcc/ada/libgnat/a-tifiio.ads index bbf8e90..0e3e71c 100644 --- a/gcc/ada/libgnat/a-tifiio.ads +++ b/gcc/ada/libgnat/a-tifiio.ads @@ -23,7 +23,10 @@ private generic type Num is delta <>; -package Ada.Text_IO.Fixed_IO with SPARK_Mode => On is +package Ada.Text_IO.Fixed_IO with + SPARK_Mode => On, + Always_Terminates +is Default_Fore : Field := Num'Fore; Default_Aft : Field := Num'Aft; @@ -34,19 +37,19 @@ package Ada.Text_IO.Fixed_IO with SPARK_Mode => On is Item : out Num; Width : Field := 0) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Exceptional_Cases => (Data_Error | End_Error => Standard.True); procedure Get (Item : out Num; Width : Field := 0) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Data_Error | End_Error => Standard.True); procedure Put (File : File_Type; @@ -55,12 +58,12 @@ package Ada.Text_IO.Fixed_IO with SPARK_Mode => On is Aft : Field := Default_Aft; Exp : Field := Default_Exp) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => Line_Length (File)'Old = Line_Length (File) and Page_Length (File)'Old = Page_Length (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Layout_Error => Line_Length (File) /= 0); procedure Put (Item : Num; @@ -68,19 +71,19 @@ package Ada.Text_IO.Fixed_IO with SPARK_Mode => On is Aft : Field := Default_Aft; Exp : Field := Default_Exp) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Layout_Error => Ada.Text_IO.Line_Length /= 0); procedure Get (From : String; Item : out Num; Last : out Positive) with - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => (Data_Error => Standard.True); procedure Put (To : out String; @@ -88,8 +91,8 @@ package Ada.Text_IO.Fixed_IO with SPARK_Mode => On is Aft : Field := Default_Aft; Exp : Field := Default_Exp) with - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => (Layout_Error => Standard.True); private pragma Inline (Get); diff --git a/gcc/ada/libgnat/a-tiflio.ads b/gcc/ada/libgnat/a-tiflio.ads index 82ff84b..fcfa76a 100644 --- a/gcc/ada/libgnat/a-tiflio.ads +++ b/gcc/ada/libgnat/a-tiflio.ads @@ -43,7 +43,10 @@ private generic type Num is digits <>; -package Ada.Text_IO.Float_IO with SPARK_Mode => On is +package Ada.Text_IO.Float_IO with + SPARK_Mode => On, + Always_Terminates +is Default_Fore : Field := 2; Default_Aft : Field := Num'Digits - 1; @@ -54,19 +57,19 @@ package Ada.Text_IO.Float_IO with SPARK_Mode => On is Item : out Num; Width : Field := 0) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Exceptional_Cases => (Data_Error | End_Error => Standard.True); procedure Get (Item : out Num; Width : Field := 0) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Data_Error | End_Error => Standard.True); procedure Put (File : File_Type; @@ -75,12 +78,12 @@ package Ada.Text_IO.Float_IO with SPARK_Mode => On is Aft : Field := Default_Aft; Exp : Field := Default_Exp) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => Line_Length (File)'Old = Line_Length (File) and Page_Length (File)'Old = Page_Length (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Layout_Error => Line_Length (File) /= 0); procedure Put (Item : Num; @@ -88,19 +91,19 @@ package Ada.Text_IO.Float_IO with SPARK_Mode => On is Aft : Field := Default_Aft; Exp : Field := Default_Exp) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Layout_Error => Line_Length /= 0); procedure Get (From : String; Item : out Num; Last : out Positive) with - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => (Data_Error => Standard.True); procedure Put (To : out String; @@ -108,8 +111,8 @@ package Ada.Text_IO.Float_IO with SPARK_Mode => On is Aft : Field := Default_Aft; Exp : Field := Default_Exp) with - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => (Layout_Error => Standard.True); private pragma Inline (Get); diff --git a/gcc/ada/libgnat/a-tiinio.ads b/gcc/ada/libgnat/a-tiinio.ads index 0299cc0..60f21cc 100644 --- a/gcc/ada/libgnat/a-tiinio.ads +++ b/gcc/ada/libgnat/a-tiinio.ads @@ -43,7 +43,9 @@ private generic type Num is range <>; -package Ada.Text_IO.Integer_IO is +package Ada.Text_IO.Integer_IO with + Always_Terminates +is Default_Width : Field := Num'Width; Default_Base : Number_Base := 10; @@ -53,19 +55,19 @@ package Ada.Text_IO.Integer_IO is Item : out Num; Width : Field := 0) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Exceptional_Cases => (Data_Error | End_Error => Standard.True); procedure Get (Item : out Num; Width : Field := 0) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Data_Error | End_Error => Standard.True); procedure Put (File : File_Type; @@ -73,39 +75,39 @@ package Ada.Text_IO.Integer_IO is Width : Field := Default_Width; Base : Number_Base := Default_Base) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => Line_Length (File)'Old = Line_Length (File) and Page_Length (File)'Old = Page_Length (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Layout_Error => Line_Length (File) /= 0); procedure Put (Item : Num; Width : Field := Default_Width; Base : Number_Base := Default_Base) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Layout_Error => Line_Length /= 0); procedure Get (From : String; Item : out Num; Last : out Positive) with - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => (Data_Error => Standard.True); procedure Put (To : out String; Item : Num; Base : Number_Base := Default_Base) with - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => (Layout_Error => Standard.True); private pragma Inline (Get); diff --git a/gcc/ada/libgnat/a-timoio.ads b/gcc/ada/libgnat/a-timoio.ads index c8554b8..40d91ed 100644 --- a/gcc/ada/libgnat/a-timoio.ads +++ b/gcc/ada/libgnat/a-timoio.ads @@ -43,7 +43,9 @@ private generic type Num is mod <>; -package Ada.Text_IO.Modular_IO is +package Ada.Text_IO.Modular_IO with + Always_Terminates +is Default_Width : Field := Num'Width; Default_Base : Number_Base := 10; @@ -53,19 +55,19 @@ package Ada.Text_IO.Modular_IO is Item : out Num; Width : Field := 0) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Exceptional_Cases => (Data_Error | End_Error => Standard.True); procedure Get (Item : out Num; Width : Field := 0) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Data_Error | End_Error => Standard.True); procedure Put (File : File_Type; @@ -73,39 +75,39 @@ package Ada.Text_IO.Modular_IO is Width : Field := Default_Width; Base : Number_Base := Default_Base) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => Line_Length (File)'Old = Line_Length (File) and Page_Length (File)'Old = Page_Length (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Layout_Error => Line_Length (File) /= 0); procedure Put (Item : Num; Width : Field := Default_Width; Base : Number_Base := Default_Base) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Layout_Error => Line_Length /= 0); procedure Get (From : String; Item : out Num; Last : out Positive) with - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => (Data_Error => Standard.True); procedure Put (To : out String; Item : Num; Base : Number_Base := Default_Base) with - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => (Layout_Error => Standard.True); private pragma Inline (Get); diff --git a/gcc/ada/libgnat/g-alleve.adb b/gcc/ada/libgnat/g-alleve.adb index b51181a..91e3ddd 100644 --- a/gcc/ada/libgnat/g-alleve.adb +++ b/gcc/ada/libgnat/g-alleve.adb @@ -643,8 +643,8 @@ package body GNAT.Altivec.Low_Level_Vectors is begin for J in Varray_Type'Range loop - All_Element := All_Element and then (D (J) = Bool_True); - Any_Element := Any_Element or else (D (J) = Bool_True); + All_Element := All_Element and then D (J) = Bool_True; + Any_Element := Any_Element or else D (J) = Bool_True; end loop; if A = CR6_LT then @@ -1089,8 +1089,8 @@ package body GNAT.Altivec.Low_Level_Vectors is begin for J in Varray_Type'Range loop - All_Element := All_Element and then (D (J) = Bool_True); - Any_Element := Any_Element or else (D (J) = Bool_True); + All_Element := All_Element and then D (J) = Bool_True; + Any_Element := Any_Element or else D (J) = Bool_True; end loop; if A = CR6_LT then @@ -1582,7 +1582,7 @@ package body GNAT.Altivec.Low_Level_Vectors is D : C_float; begin - if (Bits (VSCR, NJ_POS, NJ_POS) = 1) + if Bits (VSCR, NJ_POS, NJ_POS) = 1 and then abs (X) < 2.0 ** (-126) then D := (if X < 0.0 then -0.0 else +0.0); diff --git a/gcc/ada/libgnat/g-debpoo.adb b/gcc/ada/libgnat/g-debpoo.adb index 91c1416..93be9b1 100644 --- a/gcc/ada/libgnat/g-debpoo.adb +++ b/gcc/ada/libgnat/g-debpoo.adb @@ -362,13 +362,6 @@ package body GNAT.Debug_Pools is -- These procedures are used as markers when computing the stacktraces, -- so that addresses in the debug pool itself are not reported to the user. - Code_Address_For_Allocate_End : System.Address := System.Null_Address; - Code_Address_For_Deallocate_End : System.Address; - Code_Address_For_Dereference_End : System.Address; - -- Taking the address of the above procedures will not work on some - -- architectures (HPUX for instance). Thus we do the same thing that - -- is done in a-except.adb, and get the address of labels instead. - procedure Skip_Levels (Depth : Natural; Trace : Tracebacks_Array; @@ -906,7 +899,7 @@ package body GNAT.Debug_Pools is Set_Handled; else Ptr.Valid (Offset / System.Storage_Unit) := - Ptr.Valid (Offset / System.Storage_Unit) and (not Bit); + Ptr.Valid (Offset / System.Storage_Unit) and not Bit; end if; end if; end Set_Valid; @@ -944,8 +937,6 @@ package body GNAT.Debug_Pools is pragma Unreferenced (Lock); begin - <<Allocate_Label>> - if Disable then Storage_Address := System.CRTL.malloc (System.CRTL.size_t (Size_In_Storage_Elements)); @@ -1022,8 +1013,8 @@ package body GNAT.Debug_Pools is (Pool => Pool, Kind => Alloc, Size => Size_In_Storage_Elements, - Ignored_Frame_Start => Allocate_Label'Address, - Ignored_Frame_End => Code_Address_For_Allocate_End); + Ignored_Frame_Start => Allocate'Code_Address, + Ignored_Frame_End => Allocate_End'Code_Address); pragma Warnings (Off); -- Turn warning on alignment for convert call off. We know that in fact @@ -1073,8 +1064,8 @@ package body GNAT.Debug_Pools is Put (Output_File (Pool), "), at "); Put_Line (Output_File (Pool), Pool.Stack_Trace_Depth, null, - Allocate_Label'Address, - Code_Address_For_Deallocate_End); + Allocate'Code_Address, + Deallocate_End'Code_Address); end if; -- Update internal data @@ -1106,11 +1097,7 @@ package body GNAT.Debug_Pools is -- is done in a-except, so that we can hide the traceback frames internal -- to this package - procedure Allocate_End is - begin - <<Allocate_End_Label>> - Code_Address_For_Allocate_End := Allocate_End_Label'Address; - end Allocate_End; + procedure Allocate_End is null; ------------------- -- Set_Dead_Beef -- @@ -1476,8 +1463,6 @@ package body GNAT.Debug_Pools is Header_Block_Size_Was_Less_Than_0 : Boolean := True; begin - <<Deallocate_Label>> - declare Lock : Scope_Lock; pragma Unreferenced (Lock); @@ -1518,8 +1503,8 @@ package body GNAT.Debug_Pools is Put (Output_File (Pool), "), at "); Put_Line (Output_File (Pool), Pool.Stack_Trace_Depth, null, - Deallocate_Label'Address, - Code_Address_For_Deallocate_End); + Deallocate'Code_Address, + Deallocate_End'Code_Address); Print_Traceback (Output_File (Pool), " Memory was allocated at ", Header.Alloc_Traceback); @@ -1569,8 +1554,8 @@ package body GNAT.Debug_Pools is (Find_Or_Create_Traceback (Pool, Dealloc, Header.Block_Size, - Deallocate_Label'Address, - Code_Address_For_Deallocate_End)), + Deallocate'Code_Address, + Deallocate_End'Code_Address)), Next => System.Null_Address, Block_Size => -Header.Block_Size); @@ -1608,8 +1593,8 @@ package body GNAT.Debug_Pools is Put (Output_File (Pool), "error: Freeing Null_Address, at "); Put_Line (Output_File (Pool), Pool.Stack_Trace_Depth, null, - Deallocate_Label'Address, - Code_Address_For_Deallocate_End); + Deallocate'Code_Address, + Deallocate_End'Code_Address); return; end if; end if; @@ -1629,8 +1614,8 @@ package body GNAT.Debug_Pools is Put (Output_File (Pool), "error: Freeing not allocated storage, at "); Put_Line (Output_File (Pool), Pool.Stack_Trace_Depth, null, - Deallocate_Label'Address, - Code_Address_For_Deallocate_End); + Deallocate'Code_Address, + Deallocate_End'Code_Address); end if; elsif Header_Block_Size_Was_Less_Than_0 then @@ -1640,8 +1625,8 @@ package body GNAT.Debug_Pools is Put (Output_File (Pool), "error: Freeing already deallocated storage, at "); Put_Line (Output_File (Pool), Pool.Stack_Trace_Depth, null, - Deallocate_Label'Address, - Code_Address_For_Deallocate_End); + Deallocate'Code_Address, + Deallocate_End'Code_Address); Print_Traceback (Output_File (Pool), " Memory already deallocated at ", To_Traceback (Header.Dealloc_Traceback)); @@ -1661,11 +1646,7 @@ package body GNAT.Debug_Pools is -- This is making assumptions about code order that may be invalid ??? - procedure Deallocate_End is - begin - <<Deallocate_End_Label>> - Code_Address_For_Deallocate_End := Deallocate_End_Label'Address; - end Deallocate_End; + procedure Deallocate_End is null; ----------------- -- Dereference -- @@ -1690,8 +1671,6 @@ package body GNAT.Debug_Pools is -- now invalid pointer would appear as valid). Instead, we prefer -- optimum performance for dereferences. - <<Dereference_Label>> - if not Valid then if Pool.Raise_Exceptions then raise Accessing_Not_Allocated_Storage; @@ -1699,8 +1678,8 @@ package body GNAT.Debug_Pools is Put (Output_File (Pool), "error: Accessing not allocated storage, at "); Put_Line (Output_File (Pool), Pool.Stack_Trace_Depth, null, - Dereference_Label'Address, - Code_Address_For_Dereference_End); + Deallocate'Code_Address, + Dereference_End'Code_Address); end if; else @@ -1714,8 +1693,8 @@ package body GNAT.Debug_Pools is "error: Accessing deallocated storage, at "); Put_Line (Output_File (Pool), Pool.Stack_Trace_Depth, null, - Dereference_Label'Address, - Code_Address_For_Dereference_End); + Deallocate'Code_Address, + Dereference_End'Code_Address); Print_Traceback (Output_File (Pool), " First deallocation at ", To_Traceback (Header.Dealloc_Traceback)); Print_Traceback (Output_File (Pool), " Initial allocation at ", @@ -1735,11 +1714,7 @@ package body GNAT.Debug_Pools is -- This is making assumptions about code order that may be invalid ??? - procedure Dereference_End is - begin - <<Dereference_End_Label>> - Code_Address_For_Dereference_End := Dereference_End_Label'Address; - end Dereference_End; + procedure Dereference_End is null; ---------------- -- Print_Info -- @@ -2512,10 +2487,4 @@ package body GNAT.Debug_Pools is Put_Line (Standard_Output, S); end Stdout_Put_Line; --- Package initialization - -begin - Allocate_End; - Deallocate_End; - Dereference_End; end GNAT.Debug_Pools; diff --git a/gcc/ada/libgnat/g-debuti.ads b/gcc/ada/libgnat/g-debuti.ads index b989cd4..51a1b77 100644 --- a/gcc/ada/libgnat/g-debuti.ads +++ b/gcc/ada/libgnat/g-debuti.ads @@ -39,8 +39,8 @@ with System; package GNAT.Debug_Utilities is pragma Pure; - Address_64 : constant Boolean := Standard'Address_Size = 64; - -- Set true if 64 bit addresses (assumes only 32 and 64 are possible) + Address_64 : constant Boolean := System.Memory_Size = 2**64; + -- Set true if 64-bit addresses (assumes only 32 and 64 are possible) Address_Image_Length : constant := 13 + 10 * Boolean'Pos (Address_64); -- Length of string returned by Image function for an address diff --git a/gcc/ada/libgnat/g-dirope.adb b/gcc/ada/libgnat/g-dirope.adb index 127f6ba..3cebc9f 100644 --- a/gcc/ada/libgnat/g-dirope.adb +++ b/gcc/ada/libgnat/g-dirope.adb @@ -636,7 +636,6 @@ package body GNAT.Directory_Operations is if not Is_Open (Dir) then Free (Dir); - Dir := Null_Dir; raise Directory_Error; end if; end Open; diff --git a/gcc/ada/libgnat/g-dirope.ads b/gcc/ada/libgnat/g-dirope.ads index a3a8e46..cdb99ff 100644 --- a/gcc/ada/libgnat/g-dirope.ads +++ b/gcc/ada/libgnat/g-dirope.ads @@ -210,8 +210,7 @@ package GNAT.Directory_Operations is procedure Open (Dir : out Dir_Type; Dir_Name : Dir_Name_Str); -- Opens the directory named by Dir_Name and returns a Dir_Type value -- that refers to this directory, and is positioned at the first entry. - -- Raises Directory_Error if Dir_Name cannot be accessed. In that case - -- Dir will be set to Null_Dir. + -- Raises Directory_Error if Dir_Name cannot be accessed. procedure Close (Dir : in out Dir_Type); -- Closes the directory stream referred to by Dir. After calling Close diff --git a/gcc/ada/libgnat/g-dynhta.adb b/gcc/ada/libgnat/g-dynhta.adb index 0119b56..7a62ac8 100644 --- a/gcc/ada/libgnat/g-dynhta.adb +++ b/gcc/ada/libgnat/g-dynhta.adb @@ -56,9 +56,9 @@ package body GNAT.Dynamic_HTables is -- range of Bucket_Range_Type. return - ((Left and Mask) * Half) + (Left and Mask) * Half or - (Right and Mask); + (Right and Mask); end Hash_Two_Keys; ------------------- diff --git a/gcc/ada/libgnat/g-sercom__linux.adb b/gcc/ada/libgnat/g-sercom__linux.adb index 216092e..401ab85 100644 --- a/gcc/ada/libgnat/g-sercom__linux.adb +++ b/gcc/ada/libgnat/g-sercom__linux.adb @@ -304,7 +304,7 @@ package body GNAT.Serial_Communications is Current.c_cc (VMIN) := char'Val (0); Current.c_cc (VTIME) := char'Val (Natural (Timeout * 10)); - Current.c_lflag := Current.c_lflag or (not ICANON); + Current.c_lflag := Current.c_lflag or not ICANON; end if; Res := cfsetispeed (Current'Address, C_Data_Rate (Rate)); diff --git a/gcc/ada/libgnat/g-souinf.ads b/gcc/ada/libgnat/g-souinf.ads index b6598b5..ea65c73 100644 --- a/gcc/ada/libgnat/g-souinf.ads +++ b/gcc/ada/libgnat/g-souinf.ads @@ -41,7 +41,7 @@ package GNAT.Source_Info with Abstract_State => (Source_Code_Information with External => (Async_Writers, Async_Readers)), - Annotate => (GNATprove, Always_Return) + Always_Terminates is pragma Preelaborate; -- Note that this unit is Preelaborate, but not Pure, that's because the diff --git a/gcc/ada/libgnat/g-spipat.ads b/gcc/ada/libgnat/g-spipat.ads index 5766b3a..297afbf 100644 --- a/gcc/ada/libgnat/g-spipat.ads +++ b/gcc/ada/libgnat/g-spipat.ads @@ -58,7 +58,7 @@ -- stored in a binary compatible manner. -- GNAT.Spitbol.Patterns (files g-spipat.ads/g-spipat.adb) --- This is a completely general patterm matching package based on the +-- This is a completely general pattern matching package based on the -- pattern language of SNOBOL4, as implemented in SPITBOL. The pattern -- language is modeled on context free grammars, with context sensitive -- extensions that provide full (type 0) computational capabilities. diff --git a/gcc/ada/libgnat/i-c.adb b/gcc/ada/libgnat/i-c.adb index 4cfccf4..63aa2a2 100644 --- a/gcc/ada/libgnat/i-c.adb +++ b/gcc/ada/libgnat/i-c.adb @@ -186,7 +186,7 @@ is (Item : char_array; Trim_Nul : Boolean := True) return String is - Count : Natural := 0; + Count : Natural; From : size_t; begin @@ -200,6 +200,7 @@ is pragma Loop_Invariant (for all J in Item'First .. From when J /= From => Item (J) /= nul); + pragma Loop_Variant (Increases => From); if From > Item'Last then raise Terminator_Error; @@ -257,6 +258,7 @@ is pragma Loop_Invariant (for all J in Item'First .. From when J /= From => Item (J) /= nul); + pragma Loop_Variant (Increases => From); if From > Item'Last then raise Terminator_Error; @@ -333,6 +335,7 @@ is pragma Loop_Invariant (for all J in Item'First .. From when J /= From => Item (J) /= wide_nul); + pragma Loop_Variant (Increases => From); if From > Item'Last then raise Terminator_Error; @@ -390,6 +393,7 @@ is pragma Loop_Invariant (for all J in Item'First .. From when J /= From => Item (J) /= wide_nul); + pragma Loop_Variant (Increases => From); if From > Item'Last then raise Terminator_Error; @@ -466,6 +470,7 @@ is pragma Loop_Invariant (for all J in Item'First .. From when J /= From => Item (J) /= char16_nul); + pragma Loop_Variant (Increases => From); if From > Item'Last then raise Terminator_Error; @@ -523,6 +528,7 @@ is pragma Loop_Invariant (for all J in Item'First .. From when J /= From => Item (J) /= char16_nul); + pragma Loop_Variant (Increases => From); if From > Item'Last then raise Terminator_Error; @@ -599,6 +605,8 @@ is pragma Loop_Invariant (for all J in Item'First .. From when J /= From => Item (J) /= char32_nul); + pragma Loop_Invariant (From <= Item'First + C_Length_Ghost (Item)); + pragma Loop_Variant (Increases => From); if From > Item'Last then raise Terminator_Error; @@ -656,6 +664,7 @@ is pragma Loop_Invariant (for all J in Item'First .. From when J /= From => Item (J) /= char32_nul); + pragma Loop_Variant (Increases => From); if From > Item'Last then raise Terminator_Error; diff --git a/gcc/ada/libgnat/i-c.ads b/gcc/ada/libgnat/i-c.ads index 7013902..fe87fba 100644 --- a/gcc/ada/libgnat/i-c.ads +++ b/gcc/ada/libgnat/i-c.ads @@ -24,12 +24,14 @@ pragma Assertion_Policy (Pre => Ignore, Contract_Cases => Ignore, Ghost => Ignore); +with System; with System.Parameters; -package Interfaces.C - with SPARK_Mode, Pure +package Interfaces.C with + SPARK_Mode, + Pure, + Always_Terminates is - pragma Annotate (GNATprove, Always_Return, C); -- Each of the types declared in Interfaces.C is C-compatible. @@ -82,10 +84,9 @@ is -- a non-private system.address type. type ptrdiff_t is - range -(2 ** (System.Parameters.ptr_bits - Integer'(1))) .. - +(2 ** (System.Parameters.ptr_bits - Integer'(1)) - 1); + range -System.Memory_Size / 2 .. System.Memory_Size / 2 - 1; - type size_t is mod 2 ** System.Parameters.ptr_bits; + type size_t is mod System.Memory_Size; -- Boolean type diff --git a/gcc/ada/libgnat/i-cheri.adb b/gcc/ada/libgnat/i-cheri.adb new file mode 100644 index 0000000..174fdcc --- /dev/null +++ b/gcc/ada/libgnat/i-cheri.adb @@ -0,0 +1,75 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT COMPILER COMPONENTS -- +-- -- +-- I N T E R F A C E S . C H E R I -- +-- -- +-- S p e c -- +-- -- +-- Copyright (C) 2023, AdaCore -- +-- -- +-- 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 body Interfaces.CHERI is + + ---------------------------- + -- Set_Address_And_Bounds -- + ---------------------------- + + procedure Set_Address_And_Bounds + (Cap : in out Capability; + Address : System.Storage_Elements.Integer_Address; + Length : Bounds_Length) + is + begin + Cap := Capability_With_Address_And_Bounds (Cap, Address, Length); + end Set_Address_And_Bounds; + + ---------------------------------- + -- Set_Address_And_Exact_Bounds -- + ---------------------------------- + + procedure Set_Address_And_Exact_Bounds + (Cap : in out Capability; + Address : System.Storage_Elements.Integer_Address; + Length : Bounds_Length) + is + begin + Cap := Capability_With_Address_And_Exact_Bounds (Cap, Address, Length); + end Set_Address_And_Exact_Bounds; + + ---------------------- + -- Align_Address_Up -- + ---------------------- + + function Align_Address_Up + (Address : System.Storage_Elements.Integer_Address; + Length : Bounds_Length) + return System.Storage_Elements.Integer_Address + is + Mask : constant System.Storage_Elements.Integer_Address := + Representable_Alignment_Mask (Length); + begin + return (Address + (not Mask)) and Mask; + end Align_Address_Up; + +end Interfaces.CHERI; diff --git a/gcc/ada/libgnat/i-cheri.ads b/gcc/ada/libgnat/i-cheri.ads new file mode 100644 index 0000000..547b033 --- /dev/null +++ b/gcc/ada/libgnat/i-cheri.ads @@ -0,0 +1,470 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT COMPILER COMPONENTS -- +-- -- +-- I N T E R F A C E S . C H E R I -- +-- -- +-- S p e c -- +-- -- +-- Copyright (C) 2023, AdaCore -- +-- -- +-- 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 bindings to CHERI intrinsics and some common +-- operations on capabilities. + +with System; +with System.Storage_Elements; + +package Interfaces.CHERI with + Preelaborate, + No_Elaboration_Code_All +is + + use type System.Storage_Elements.Integer_Address; + + subtype Capability is System.Address; + + type Bounds_Length is range 0 .. System.Memory_Size - 1 with + Size => System.Word_Size; + + ---------------------------- + -- Capability Permissions -- + ---------------------------- + + type Permissions_Mask is mod System.Memory_Size with + Size => System.Word_Size; + + Global : constant Permissions_Mask := 16#0001#; + Executive : constant Permissions_Mask := 16#0002#; + Mutable_Load : constant Permissions_Mask := 16#0040#; + Compartment_Id : constant Permissions_Mask := 16#0080#; + Branch_Sealed_Pair : constant Permissions_Mask := 16#0100#; + Access_System_Registers : constant Permissions_Mask := 16#0200#; + Permit_Unseal : constant Permissions_Mask := 16#0400#; + Permit_Seal : constant Permissions_Mask := 16#0800#; + Permit_Store_Local : constant Permissions_Mask := 16#1000#; + Permit_Store_Capability : constant Permissions_Mask := 16#2000#; + Permit_Load_Capability : constant Permissions_Mask := 16#4000#; + Permit_Execute : constant Permissions_Mask := 16#8000#; + Permit_Store : constant Permissions_Mask := 16#1_0000#; + Permit_Load : constant Permissions_Mask := 16#2_0000#; + + function "and" + (Cap : Capability; + Mask : Permissions_Mask) + return Capability + with + Import, Convention => Intrinsic, + External_Name => "__builtin_cheri_perms_and"; + -- Perform a bitwise-AND of a capability permissions and the specified + -- mask, returning the new capability. + + function Get_Permissions (Cap : Capability) return Permissions_Mask with + Import, Convention => Intrinsic, + External_Name => "__builtin_cheri_perms_get"; + -- Get the permissions of a capability + + function Clear_Permissions + (Cap : Capability; + Mask : Permissions_Mask) + return Capability is + (Cap and not Mask); + -- Clear the specified permissions of a capability, returning the new + -- capability. + + function Has_All_Permissions + (Cap : Capability; + Permissions : Permissions_Mask) + return Boolean is + ((Get_Permissions (Cap) and Permissions) = Permissions); + -- Query whether all of the specified permission bits are set in a + -- capability's permissions flags. + + ----------------------- + -- Common Intrinsics -- + ----------------------- + + function Capability_With_Address + (Cap : Capability; + Addr : System.Storage_Elements.Integer_Address) + return Capability + with + Import, Convention => Intrinsic, + External_Name => "__builtin_cheri_address_set"; + -- Return a new capability with the same bounds and permissions as Cap, + -- with the address set to Addr. + + function Get_Address + (Cap : Capability) + return System.Storage_Elements.Integer_Address + with + Import, Convention => Intrinsic, + External_Name => "__builtin_cheri_address_get"; + -- Get the address of a capability + + procedure Set_Address + (Cap : in out Capability; + Addr : System.Storage_Elements.Integer_Address) + with + Import, Convention => Intrinsic, + External_Name => "__builtin_cheri_address_set"; + -- Set the address of a capability + + function Get_Base + (Cap : Capability) + return System.Storage_Elements.Integer_Address + with + Import, Convention => Intrinsic, + External_Name => "__builtin_cheri_base_get"; + -- Get the lower bound of a capability + + function Get_Offset (Cap : Capability) return Bounds_Length with + Import, Convention => Intrinsic, + External_Name => "__builtin_cheri_offset_get"; + -- Get the difference between the address and the lower bound of a + -- capability. + + procedure Set_Offset + (Cap : in out Capability; + Offset : Bounds_Length) + with + Import, Convention => Intrinsic, + External_Name => "__builtin_cheri_offset_set"; + -- Set the address relative to the lower bound of a capability + + function Capability_With_Offset + (Cap : Capability; + Value : Bounds_Length) + return Capability + with + Import, Convention => Intrinsic, + External_Name => "__builtin_cheri_offset_set"; + -- Set the address relative to the lower bound of a capability, returning + -- the new capability. + + function Increment_Offset + (Cap : Capability; + Value : Bounds_Length) + return Capability + with + Import, Convention => Intrinsic, + External_Name => "__builtin_cheri_offset_increment"; + -- Increment the address of a capability by the specified amount, + -- returning the new capability. + + function Get_Length (Cap : Capability) return Bounds_Length with + Import, Convention => Intrinsic, + External_Name => "__builtin_cheri_length_get"; + -- Get the length of a capability's bounds + + function Clear_Tag (Cap : Capability) return Capability with + Import, Convention => Intrinsic, + External_Name => "__builtin_cheri_tag_clear"; + -- Clear the capability validity tag, returning the new capability + + function Get_Tag (Cap : Capability) return Boolean with + Import, Convention => Intrinsic, + External_Name => "__builtin_cheri_tag_get"; + -- Get the validty tag of a capability + + function Is_Valid (Cap : Capability) return Boolean is (Get_Tag (Cap)); + -- Check whether a capability is valid + + function Is_Invalid (Cap : Capability) return Boolean is + (not Is_Valid (Cap)); + -- Check whether a capability is invalid + + function Is_Equal_Exact (A, B : Capability) return Boolean with + Import, Convention => Intrinsic, + External_Name => "__builtin_cheri_equal_exact"; + -- Check for bit equality between two capabilities + + function Is_Subset (A, B : Capability) return Boolean with + Import, Convention => Intrinsic, + External_Name => "__builtin_cheri_subset_test"; + -- Returns True if capability A is a subset or equal to capability B + + -------------------- + -- Bounds Setting -- + -------------------- + + function Capability_With_Bounds + (Cap : Capability; + Length : Bounds_Length) + return Capability + with + Import, Convention => Intrinsic, + External_Name => "__builtin_cheri_bounds_set"; + -- Narrow the bounds of a capability so that the lower bound is the + -- current address and the upper bound is suitable for the Length, + -- returning the new capability. + -- + -- Note that the effective bounds of the returned capability may be wider + -- than the range Get_Address (Cap) .. Get_Address (Cap) + Length - 1 due + -- to capability compression, but they will always be a subset of the + -- original bounds. + + function Capability_With_Exact_Bounds + (Cap : Capability; + Length : Bounds_Length) + return Capability + with + Import, Convention => Intrinsic, + External_Name => "__builtin_cheri_bounds_set_exact"; + -- Narrow the bounds of a capability so that the lower bound is the + -- current address and the upper bound is suitable for the Length, + -- returning the new capability. + -- + -- This is similar to Capability_With_Bounds but will clear the capability + -- tag in the returned capability if the bounds cannot be set exactly, due + -- to capability compression. + + function Capability_With_Address_And_Bounds + (Cap : Capability; + Address : System.Storage_Elements.Integer_Address; + Length : Bounds_Length) + return Capability is + (Capability_With_Bounds + (Capability_With_Address (Cap, Address), Length)); + -- Set the address and narrow the bounds of the capability so that the + -- lower bound is Address and the upper bound is Address + Length, + -- returning the new capability. + -- + -- Note that the effective bounds of the returned capability may be wider + -- than the range Address .. Address + Length - 1 due to capability + -- compression, but they will always be a subset of the original bounds. + + function Capability_With_Address_And_Exact_Bounds + (Cap : Capability; + Address : System.Storage_Elements.Integer_Address; + Length : Bounds_Length) + return Capability is + (Capability_With_Exact_Bounds + (Capability_With_Address (Cap, Address), Length)); + -- Set the address and narrow the bounds of the capability so that the + -- lower bound is Address and the upper bound is Address + Length, + -- returning the new capability. + -- + -- This is similar to Capability_With_Address_And_Bounds but will clear the + -- capability tag in the returned capability if the bounds cannot be set + -- exactly, due to capability compression. + + procedure Set_Bounds + (Cap : in out Capability; + Length : Bounds_Length) + with + Import, Convention => Intrinsic, + External_Name => "__builtin_cheri_bounds_set"; + -- Narrow the bounds of a capability so that the lower bound is the + -- current address and the upper bound is suitable for the Length. + -- + -- Note that the effective bounds of the output capability may be wider + -- than the range Get_Address (Cap) .. Get_Address (Cap) + Length - 1 due + -- to capability compression, but they will always be a subset of the + -- original bounds. + + procedure Set_Exact_Bounds + (Cap : in out Capability; + Length : Bounds_Length) + with + Import, Convention => Intrinsic, + External_Name => "__builtin_cheri_bounds_set_exact"; + -- Narrow the bounds of a capability so that the lower bound is the + -- current address and the upper bound is suitable for the Length. + -- + -- This is similar to Set_Bounds but will clear the capability tag if the + -- bounds cannot be set exactly, due to capability compression. + + procedure Set_Address_And_Bounds + (Cap : in out Capability; + Address : System.Storage_Elements.Integer_Address; + Length : Bounds_Length) + with + Inline_Always; + -- Set the address and narrow the bounds of the capability so that the + -- lower bound is Address and the upper bound is Address + Length. + -- + -- Note that the effective bounds of the output capability may be wider + -- than the range Address .. Address + Length - 1 due to capability + -- compression, but they will always be a subset of the original bounds. + + procedure Set_Address_And_Exact_Bounds + (Cap : in out Capability; + Address : System.Storage_Elements.Integer_Address; + Length : Bounds_Length) + with + Inline_Always; + -- Set the address and narrow the bounds of the capability so that the + -- lower bound is Address and the upper bound is Address + Length. + -- + -- This is similar to Set_Address_And_Bounds but will clear the capability + -- tag if the bounds cannot be set exactly, due to capability compression. + + function Representable_Length (Length : Bounds_Length) return Bounds_Length + with + Import, Convention => Intrinsic, + External_Name => "__builtin_cheri_round_representable_length"; + -- Returns the length that a capability would have after using Set_Bounds + -- to set the Length (assuming appropriate alignment of the base). + + function Representable_Alignment_Mask + (Length : Bounds_Length) + return System.Storage_Elements.Integer_Address + with + Import, Convention => Intrinsic, + External_Name => "__builtin_cheri_representable_alignment_mask"; + -- Returns a bitmask that can be used to align an address downwards such + -- that it is sufficiently aligned to create a precisely bounded + -- capability. + + function Align_Address_Down + (Address : System.Storage_Elements.Integer_Address; + Length : Bounds_Length) + return System.Storage_Elements.Integer_Address is + (Address and Representable_Alignment_Mask (Length)); + -- Align an address such that it is sufficiently aligned to create a + -- precisely bounded capability, rounding down if necessary. + -- + -- Due to capability compression, the upper and lower bounds of a + -- capability must be aligned based on the length of the bounds to ensure + -- that the capability is representable. This function aligns an address + -- down to the next boundary if it is not already aligned. + + function Capability_With_Address_Aligned_Down + (Cap : Capability; + Length : Bounds_Length) + return Capability is + (Capability_With_Address + (Cap, Align_Address_Down (Get_Address (Cap), Length))); + -- Align a capability's address such that it is sufficiently aligned to + -- create a precisely bounded capability, rounding down if necessary. + -- + -- Due to capability compression, the upper and lower bounds of a + -- capability must be aligned based on the length of the bounds to ensure + -- that the capability is representable. This function aligns an address + -- down to the next boundary if it is not already aligned. + + function Align_Address_Up + (Address : System.Storage_Elements.Integer_Address; + Length : Bounds_Length) + return System.Storage_Elements.Integer_Address + with + Inline; + -- Align an address such that it is sufficiently aligned to create a + -- precisely bounded capability, rounding upwards if necessary. + -- + -- Due to capability compression, the upper and lower bounds of a + -- capability must be aligned based on the length of the bounds to ensure + -- that the capability is representable. This function aligns an address up + -- to the next boundary if it is not already aligned. + + function Capability_With_Address_Aligned_Up + (Cap : Capability; + Length : Bounds_Length) + return Capability is + (Capability_With_Address + (Cap, Align_Address_Up (Get_Address (Cap), Length))); + -- Align a capability's address such that it is sufficiently aligned to + -- create a precisely bounded capability, rounding upwards if necessary. + -- + -- Due to capability compression, the upper and lower bounds of a + -- capability must be aligned based on the length of the bounds to ensure + -- that the capability is representable. This function aligns an address up + -- to the next boundary if it is not already aligned. + + ------------------------------------------ + -- Object Types, Sealing, and Unsealing -- + ------------------------------------------ + + type Object_Type is + range -2**(System.Word_Size - 1) .. +2**(System.Word_Size - 1) - 1 with + Size => System.Word_Size; + + Type_Unsealed : constant Object_Type := 0; + Type_Sentry : constant Object_Type := 1; + + function Get_Object_Type (Cap : Capability) return Object_Type with + Import, Convention => Intrinsic, + External_Name => "__builtin_cheri_type_get"; + -- Get the object type of a capability + + function Is_Sealed (Cap : Capability) return Boolean with + Import, Convention => Intrinsic, + External_Name => "__builtin_cheri_sealed_get"; + -- Check whether a capability is sealed + + function Is_Unsealed (Cap : Capability) return Boolean is + (not Is_Sealed (Cap)); + -- Check whether a capability is unsealed + + function Is_Sentry (Cap : Capability) return Boolean is + (Get_Object_Type (Cap) = Type_Sentry); + -- Check whether a capability is a sealed entry + + function Create_Sentry (Cap : Capability) return Capability with + Import, Convention => Intrinsic, + External_Name => "__builtin_cheri_seal_entry"; + -- Create a sealed entry and return the new capability. + + function Seal + (Cap : Capability; + Sealing_Cap : Capability) + return Capability + with + Import, Convention => Intrinsic, + External_Name => "__builtin_cheri_seal"; + -- Seal a capability with a sealing capability, by setting the object type + -- of the capability to the Sealing_Cap's value, returning the sealed + -- capability. + + function Unseal + (Cap : Capability; + Unsealing_Cap : Capability) + return Capability + with + Import, Convention => Intrinsic, + External_Name => "__builtin_cheri_unseal"; + -- Unseal a capability with an unsealing capability, by checking the object + -- type of the capability against the Sealing_Cap's value, returning the + -- unsealed capability. + + ----------------------------------- + -- Capability Register Accessors -- + ----------------------------------- + + function Get_PCC return System.Address with + Import, Convention => Intrinsic, + External_Name => "__builtin_cheri_program_counter_get"; + -- Get the Program Counter Capablity (PCC) + + function Get_DDC return System.Address with + Import, Convention => Intrinsic, + External_Name => "__builtin_cheri_global_data_get"; + -- Get the Default Data Capability (DDC) + + function Get_CSP return System.Address with + Import, Convention => Intrinsic, + External_Name => "__builtin_cheri_stack_get"; + -- Get the Capability Stack Pointer (CSP) + +end Interfaces.CHERI; diff --git a/gcc/ada/libgnat/i-cpoint.adb b/gcc/ada/libgnat/i-cpoint.adb index bf08e1a..e1805f4 100644 --- a/gcc/ada/libgnat/i-cpoint.adb +++ b/gcc/ada/libgnat/i-cpoint.adb @@ -29,19 +29,20 @@ -- -- ------------------------------------------------------------------------------ -with Interfaces.C.Strings; use Interfaces.C.Strings; -with System; use System; +with Interfaces.C.Strings; use Interfaces.C.Strings; +with System.Storage_Elements; use System.Storage_Elements; +with System; use System; with Ada.Unchecked_Conversion; package body Interfaces.C.Pointers is - type Addr is mod 2 ** System.Parameters.ptr_bits; + subtype Offset is Storage_Offset; - function To_Pointer is new Ada.Unchecked_Conversion (Addr, Pointer); - function To_Addr is new Ada.Unchecked_Conversion (Pointer, Addr); - function To_Addr is new Ada.Unchecked_Conversion (ptrdiff_t, Addr); - function To_Ptrdiff is new Ada.Unchecked_Conversion (Addr, ptrdiff_t); + function To_Pointer is new Ada.Unchecked_Conversion (Address, Pointer); + function To_Addr is new Ada.Unchecked_Conversion (Pointer, Address); + function To_Offset is new Ada.Unchecked_Conversion (ptrdiff_t, Offset); + function To_Ptrdiff is new Ada.Unchecked_Conversion (Offset, ptrdiff_t); Elmt_Size : constant ptrdiff_t := (Element_Array'Component_Size @@ -59,7 +60,7 @@ package body Interfaces.C.Pointers is raise Pointer_Error; end if; - return To_Pointer (To_Addr (Left) + To_Addr (Elmt_Size * Right)); + return To_Pointer (To_Addr (Left) + To_Offset (Elmt_Size * Right)); end "+"; function "+" (Left : ptrdiff_t; Right : Pointer) return Pointer is @@ -68,7 +69,7 @@ package body Interfaces.C.Pointers is raise Pointer_Error; end if; - return To_Pointer (To_Addr (Elmt_Size * Left) + To_Addr (Right)); + return To_Pointer (To_Offset (Elmt_Size * Left) + To_Addr (Right)); end "+"; --------- @@ -81,7 +82,7 @@ package body Interfaces.C.Pointers is raise Pointer_Error; end if; - return To_Pointer (To_Addr (Left) - To_Addr (Right * Elmt_Size)); + return To_Pointer (To_Addr (Left) - To_Offset (Right * Elmt_Size)); end "-"; function "-" (Left : Pointer; Right : Pointer) return ptrdiff_t is diff --git a/gcc/ada/libgnat/i-cstrin.ads b/gcc/ada/libgnat/i-cstrin.ads index 0f39cd8..e486f03 100644 --- a/gcc/ada/libgnat/i-cstrin.ads +++ b/gcc/ada/libgnat/i-cstrin.ads @@ -44,7 +44,8 @@ pragma Assertion_Policy (Pre => Ignore); package Interfaces.C.Strings with SPARK_Mode => On, Abstract_State => (C_Memory), - Initializes => (C_Memory) + Initializes => (C_Memory), + Always_Terminates is pragma Preelaborate; @@ -67,7 +68,7 @@ is (Item : char_array_access; Nul_Check : Boolean := False) return chars_ptr with - SPARK_Mode => Off; + SPARK_Mode => Off; -- To_Chars_Ptr'Result is aliased with Item function New_Char_Array (Chars : char_array) return chars_ptr with Volatile_Function, @@ -120,10 +121,8 @@ is with Pre => Item /= Null_Ptr - and then - (if Check then - Strlen (Item) <= size_t'Last - Offset - and then Strlen (Item) + Offset <= Chars'Length), + and then Strlen (Item) <= size_t'Last - Offset + and then Strlen (Item) + Offset <= Chars'Length, Global => (In_Out => C_Memory); procedure Update @@ -134,10 +133,8 @@ is with Pre => Item /= Null_Ptr - and then - (if Check then - Strlen (Item) <= size_t'Last - Offset - and then Strlen (Item) + Offset <= Str'Length), + and then Strlen (Item) <= size_t'Last - Offset + and then Strlen (Item) + Offset <= Str'Length, Global => (In_Out => C_Memory); Update_Error : exception; diff --git a/gcc/ada/libgnat/interfac.ads b/gcc/ada/libgnat/interfac.ads index edd3f36..bc37a8e 100644 --- a/gcc/ada/libgnat/interfac.ads +++ b/gcc/ada/libgnat/interfac.ads @@ -35,10 +35,11 @@ -- This is the compiler version of this unit -package Interfaces is +package Interfaces with + Always_Terminates +is pragma No_Elaboration_Code_All; pragma Pure; - pragma Annotate (GNATprove, Always_Return, Interfaces); -- All identifiers in this unit are implementation defined diff --git a/gcc/ada/libgnat/interfac__2020.ads b/gcc/ada/libgnat/interfac__2020.ads index 89557bf..70d82be 100644 --- a/gcc/ada/libgnat/interfac__2020.ads +++ b/gcc/ada/libgnat/interfac__2020.ads @@ -35,10 +35,11 @@ -- This is the runtime version of this unit (not used during GNAT build) -package Interfaces is +package Interfaces with + Always_Terminates +is pragma No_Elaboration_Code_All; pragma Pure; - pragma Annotate (GNATprove, Always_Return, Interfaces); -- All identifiers in this unit are implementation defined diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb index 67ebdd4..831590c 100644 --- a/gcc/ada/libgnat/s-aridou.adb +++ b/gcc/ada/libgnat/s-aridou.adb @@ -45,7 +45,8 @@ is Contract_Cases => Ignore, Ghost => Ignore, Loop_Invariant => Ignore, - Assert => Ignore); + Assert => Ignore, + Assert_And_Cut => Ignore); pragma Suppress (Overflow_Check); pragma Suppress (Range_Check); @@ -138,16 +139,11 @@ is (Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (X1)) + Big_2xxSingle * Big (Double_Uns (X2)) + Big (Double_Uns (X3))) - with Ghost; + with + Ghost, + Annotate => (GNATprove, Inline_For_Proof); -- X1&X2&X3 as a big integer - function Big3 (X1, X2, X3 : Big_Integer) return Big_Integer is - (Big_2xxSingle * Big_2xxSingle * X1 - + Big_2xxSingle * X2 - + X3) - with Ghost; - -- Version of Big3 on big integers - function Le3 (X1, X2, X3, Y1, Y2, Y3 : Single_Uns) return Boolean with Post => Le3'Result = (Big3 (X1, X2, X3) <= Big3 (Y1, Y2, Y3)); @@ -169,9 +165,8 @@ is function To_Neg_Int (A : Double_Uns) return Double_Int with - Annotate => (GNATprove, Always_Return), - Pre => In_Double_Int_Range (-Big (A)), - Post => Big (To_Neg_Int'Result) = -Big (A); + Pre => In_Double_Int_Range (-Big (A)), + Post => Big (To_Neg_Int'Result) = -Big (A); -- Convert to negative integer equivalent. If the input is in the range -- 0 .. 2 ** (Double_Size - 1), then the corresponding nonpositive signed -- integer (obtained by negating the given value) is returned, otherwise @@ -179,9 +174,8 @@ is function To_Pos_Int (A : Double_Uns) return Double_Int with - Annotate => (GNATprove, Always_Return), - Pre => In_Double_Int_Range (Big (A)), - Post => Big (To_Pos_Int'Result) = Big (A); + Pre => In_Double_Int_Range (Big (A)), + Post => Big (To_Pos_Int'Result) = Big (A); -- Convert to positive integer equivalent. If the input is in the range -- 0 .. 2 ** (Double_Size - 1) - 1, then the corresponding non-negative -- signed integer is returned, otherwise constraint error is raised. @@ -1069,17 +1063,10 @@ is T1 := Ylo * Zlo; - pragma Assert (Big (T2) = Big (Double_Uns'(Yhi * Zlo)) - + Big (Double_Uns'(Ylo * Zhi))); Lemma_Mult_Distribution (Big_2xxSingle, Big (Double_Uns'(Yhi * Zlo)), Big (Double_Uns'(Ylo * Zhi))); - pragma Assert (Mult = Big_2xxSingle * Big (T2) + Big (T1)); Lemma_Hi_Lo (T1, Hi (T1), Lo (T1)); - pragma Assert - (Mult = Big_2xxSingle * Big (T2) - + Big_2xxSingle * Big (Double_Uns (Hi (T1))) - + Big (Double_Uns (Lo (T1)))); Lemma_Mult_Distribution (Big_2xxSingle, Big (T2), Big (Double_Uns (Hi (T1)))); @@ -1087,17 +1074,11 @@ is T2 := T2 + Hi (T1); - pragma Assert - (Mult = Big_2xxSingle * Big (T2) + Big (Double_Uns (Lo (T1)))); Lemma_Hi_Lo (T2, Hi (T2), Lo (T2)); Lemma_Mult_Distribution (Big_2xxSingle, Big (Double_Uns (Hi (T2))), Big (Double_Uns (Lo (T2)))); Lemma_Double_Big_2xxSingle; - pragma Assert - (Mult = Big_2xxDouble * Big (Double_Uns (Hi (T2))) - + Big_2xxSingle * Big (Double_Uns (Lo (T2))) - + Big (Double_Uns (Lo (T1)))); if Hi (T2) /= 0 then R := X; @@ -1543,15 +1524,36 @@ is Post => X / Double_Uns'(2) ** I / Double_Uns'(2) = X / Double_Uns'(2) ** (I + 1); + procedure Lemma_Quot_Rem (X, Div, Q, R : Double_Uns) + with + Ghost, + Pre => Div /= 0 + and then X = Q * Div + R + and then Q <= Double_Uns'Last / Div + and then R <= Double_Uns'Last - Q * Div + and then R < Div, + Post => Q = X / Div; + pragma Annotate (GNATprove, False_Positive, "postcondition might fail", + "Q is the quotient of X by Div"); + procedure Lemma_Div_Pow2 (X : Double_Uns; I : Natural) is Div1 : constant Double_Uns := Double_Uns'(2) ** I; Div2 : constant Double_Uns := Double_Uns'(2); Left : constant Double_Uns := X / Div1 / Div2; + R2 : constant Double_Uns := X / Div1 - Left * Div2; + pragma Assert (R2 <= Div2 - 1); + R1 : constant Double_Uns := X - X / Div1 * Div1; + pragma Assert (R1 < Div1); begin + pragma Assert (X = Left * (Div1 * Div2) + R2 * Div1 + R1); + pragma Assert (R2 * Div1 + R1 < Div1 * Div2); + Lemma_Quot_Rem (X, Div1 * Div2, Left, R2 * Div1 + R1); pragma Assert (Left = X / (Div1 * Div2)); pragma Assert (Div1 * Div2 = Double_Uns'(2) ** (I + 1)); end Lemma_Div_Pow2; + procedure Lemma_Quot_Rem (X, Div, Q, R : Double_Uns) is null; + XX : Double_Uns := X; begin @@ -1932,7 +1934,9 @@ is + Big_2xxSingle * Big_2xxSingle * D2 + Big_2xxSingle * D3 + D4) - with Ghost; + with + Ghost, + Annotate => (GNATprove, Inline_For_Proof); function Is_Scaled_Mult_Decomposition (D1, D2, D3, D4 : Big_Integer) @@ -1945,7 +1949,8 @@ is + D4) with Ghost, - Pre => Scale < Double_Size; + Annotate => (GNATprove, Inline_For_Proof), + Pre => Scale < Double_Size; -- Local lemmas @@ -2115,12 +2120,15 @@ is -- fourth component. procedure Prove_Scaled_Mult_Decomposition_Regroup3 - (D1, D2, D3, D4 : Big_Integer) + (D1, D2, D3, D4 : Single_Uns) with Ghost, Pre => Scale < Double_Size - and then Is_Scaled_Mult_Decomposition (D1, D2, D3, D4), - Post => Is_Scaled_Mult_Decomposition (0, 0, Big3 (D1, D2, D3), D4); + and then Is_Scaled_Mult_Decomposition + (Big (Double_Uns (D1)), Big (Double_Uns (D2)), + Big (Double_Uns (D3)), Big (Double_Uns (D4))), + Post => Is_Scaled_Mult_Decomposition (0, 0, Big3 (D1, D2, D3), + Big (Double_Uns (D4))); -- Proves scaled decomposition of Mult after regrouping on third -- component. @@ -2221,17 +2229,8 @@ is pragma Assert (Big_D3 = Big_T2); pragma Assert (Big_2xxSingle * Big_D3 = Big_2xxSingle * Big_T2); Lemma_Mult_Commutation (2 ** Scale, Double_Uns (D (4)), T3); - pragma Assert (Big_D4 = Big_T3); pragma Assert - (By (Is_Scaled_Mult_Decomposition (0, Big_T1, Big_T2, Big_T3), - By (Big_2xxSingle * Big_2xxSingle * Big_D12 = - Big_2xxSingle * Big_2xxSingle * Big_T1, - Big_D12 = Big_T1) - and then - By (Big_2xxSingle * Big_D3 = Big_2xxSingle * Big_T2, - Big_D3 = Big_T2) - and then - Big_D4 = Big_T3)); + (Is_Scaled_Mult_Decomposition (0, Big_T1, Big_T2, Big_T3)); Lemma_Hi_Lo (T1, Hi (T1), Lo (T1)); Lemma_Hi_Lo (T2, Hi (T2), Lo (T2)); Lemma_Hi_Lo (T3, Hi (T3), Lo (T3)); @@ -2247,60 +2246,6 @@ is Lemma_Mult_Distribution (Big_2xxSingle, Big (Double_Uns (Lo (T2))), Big (Double_Uns (Hi (T3)))); - pragma Assert - (By (Is_Scaled_Mult_Decomposition - (Big (Double_Uns (Hi (T1))), - Big (Double_Uns (Lo (T1))) + Big (Double_Uns (Hi (T2))), - Big (Double_Uns (Lo (T2))) + Big (Double_Uns (Hi (T3))), - Big (Double_Uns (Lo (T3)))), - -- Start from stating equality between the expanded values of - -- the right-hand side in the known and desired assertions over - -- Is_Scaled_Mult_Decomposition. - By (Big_2xxSingle * Big_2xxSingle * Big_2xxSingle * - Big (Double_Uns (Hi (T1))) - + Big_2xxSingle * Big_2xxSingle * - (Big (Double_Uns (Lo (T1))) + Big (Double_Uns (Hi (T2)))) - + Big_2xxSingle * - (Big (Double_Uns (Lo (T2))) + Big (Double_Uns (Hi (T3)))) - + Big (Double_Uns (Lo (T3))) = - Big_2xxSingle * Big_2xxSingle * Big_2xxSingle * 0 - + Big_2xxSingle * Big_2xxSingle * Big_T1 - + Big_2xxSingle * Big_T2 - + Big_T3, - -- Now list all known equalities that contribute - Big_2xxSingle * Big_2xxSingle * Big_2xxSingle * - Big (Double_Uns (Hi (T1))) - + Big_2xxSingle * Big_2xxSingle * - (Big (Double_Uns (Lo (T1))) + Big (Double_Uns (Hi (T2)))) - + Big_2xxSingle * - (Big (Double_Uns (Lo (T2))) + Big (Double_Uns (Hi (T3)))) - + Big (Double_Uns (Lo (T3))) = - Big_2xxSingle * Big_2xxSingle * Big_2xxSingle * - Big (Double_Uns (Hi (T1))) - + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Lo (T1))) - + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2))) - + Big_2xxSingle * Big (Double_Uns (Lo (T2))) - + Big_2xxSingle * Big (Double_Uns (Hi (T3))) - + Big (Double_Uns (Lo (T3))) - and then - By (Big_2xxSingle * Big_2xxSingle * Big (T1) - = Big_2xxSingle * Big_2xxSingle * Big_2xxSingle - * Big (Double_Uns (Hi (T1))) - + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Lo (T1))), - Big_2xxSingle * Big_2xxSingle * Big (T1) - = Big_2xxSingle * Big_2xxSingle - * (Big_2xxSingle * Big (Double_Uns (Hi (T1))) - + Big (Double_Uns (Lo (T1))))) - and then - By (Big_2xxSingle * Big (T2) - = Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2))) - + Big_2xxSingle * Big (Double_Uns (Lo (T2))), - Big_2xxSingle * Big (T2) - = Big_2xxSingle * (Big_2xxSingle * Big (Double_Uns (Hi (T2))) - + Big (Double_Uns (Lo (T2))))) - and then - Big (T3) = Big_2xxSingle * Big (Double_Uns (Hi (T3))) - + Big (Double_Uns (Lo (T3)))))); Lemma_Mult_Distribution (Big_2xxSingle * Big_2xxSingle, Big (Double_Uns (Lo (T1))), Big (Double_Uns (Hi (T2)))); @@ -2310,24 +2255,6 @@ is Double_Uns (Lo (T2)) + Double_Uns (Hi (T3))); Lemma_Add_Commutation (Double_Uns (Lo (T1)), Hi (T2)); Lemma_Add_Commutation (Double_Uns (Lo (T2)), Hi (T3)); - pragma Assert - (By (Is_Scaled_Mult_Decomposition - (Big (Double_Uns (Hi (T1))), - Big (Double_Uns (Lo (T1) or Hi (T2))), - Big (Double_Uns (Lo (T2) or Hi (T3))), - Big (Double_Uns (Lo (T3)))), - By (Big_2xxSingle * Big_2xxSingle - * Big (Double_Uns (Lo (T1) or Hi (T2))) = - Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Lo (T1))) - + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2))), - Big_2xxSingle * Big_2xxSingle - * Big (Double_Uns (Lo (T1)) + Double_Uns (Hi (T2))) = - Big_2xxSingle * Big_2xxSingle - * (Big (Double_Uns (Lo (T1))) + Big (Double_Uns (Hi (T2))))) - and then - Big_2xxSingle * Big (Double_Uns (Lo (T2) or Hi (T3))) = - Big_2xxSingle * Big (Double_Uns (Lo (T2))) - + Big_2xxSingle * Big (Double_Uns (Hi (T3))))); end Prove_Dividend_Scaling; -------------------------- @@ -2342,13 +2269,30 @@ is Lemma_Hi_Lo (T3, Hi (T3), S2); Lemma_Mult_Commutation (Double_Uns (Q), Double_Uns (Lo (Zu)), T1); Lemma_Mult_Commutation (Double_Uns (Q), Double_Uns (Hi (Zu)), T2); - pragma Assert (Big (Double_Uns (Q)) * Big (Zu) = - Big_2xxSingle * Big (T2) + Big (T1)); + Lemma_Mult_Distribution (Big (Double_Uns (Q)), + Big_2xxSingle * Big (Double_Uns (Hi (Zu))), + Big (Double_Uns (Lo (Zu)))); + Lemma_Substitution + (Big (Double_Uns (Q)) * Big (Zu), + Big (Double_Uns (Q)), + Big (Zu), + Big_2xxSingle * Big (Double_Uns (Hi (Zu))) + + Big (Double_Uns (Lo (Zu))), + Big_0); pragma Assert (Big (Double_Uns (Q)) * Big (Zu) = Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2))) - + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T3))) - + Big_2xxSingle * Big (Double_Uns (S2)) + + Big_2xxSingle * Big (Double_Uns (Lo (T2))) + + Big_2xxSingle * Big (Double_Uns (Hi (T1))) + Big (Double_Uns (S3))); + Lemma_Add_Commutation (Double_Uns (Lo (T2)), Hi (T1)); + pragma Assert + (By (Big (Double_Uns (Q)) * Big (Zu) = + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2))) + + Big_2xxSingle * Big (T3) + + Big (Double_Uns (S3)), + Big_2xxSingle * Big (Double_Uns (Lo (T2))) + + Big_2xxSingle * Big (Double_Uns (Hi (T1))) + = Big_2xxSingle * Big (T3))); pragma Assert (Double_Uns (Hi (T3)) + Hi (T2) = Double_Uns (S1)); Lemma_Add_Commutation (Double_Uns (Hi (T3)), Hi (T2)); pragma Assert @@ -2357,20 +2301,6 @@ is Lemma_Mult_Distribution (Big_2xxSingle * Big_2xxSingle, Big (Double_Uns (Hi (T3))), Big (Double_Uns (Hi (T2)))); - pragma Assert - (Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2))) - + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T3))) - = Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (S1))); - pragma Assert (Big (Double_Uns (Q)) * Big (Zu) = - Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (S1)) - + Big_2xxSingle * Big (Double_Uns (S2)) - + Big (Double_Uns (S3))); - pragma Assert - (By (Big (Double_Uns (Q)) * Big (Zu) = Big3 (S1, S2, S3), - Big3 (S1, S2, S3) = - Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (S1)) - + Big_2xxSingle * Big (Double_Uns (S2)) - + Big (Double_Uns (S3)))); end Prove_Multiplication; ------------------------------------- @@ -2492,7 +2422,7 @@ is ---------------------------------------------- procedure Prove_Scaled_Mult_Decomposition_Regroup3 - (D1, D2, D3, D4 : Big_Integer) + (D1, D2, D3, D4 : Single_Uns) is null; ------------------ @@ -2578,58 +2508,25 @@ is Lemma_Abs_Commutation (X); Lemma_Abs_Commutation (Y); Lemma_Mult_Decomposition (Mult, Xu, Yu, Xhi, Xlo, Yhi, Ylo); - pragma Assert - (Is_Mult_Decomposition - (D1 => 0, - D2 => Big (Double_Uns'(Xhi * Yhi)), - D3 => Big (Double_Uns'(Xhi * Ylo)) + Big (Double_Uns'(Xlo * Yhi)), - D4 => Big (Double_Uns'(Xlo * Ylo)))); T1 := Xlo * Ylo; D (4) := Lo (T1); D (3) := Hi (T1); Lemma_Hi_Lo (T1, D (3), D (4)); - pragma Assert - (Is_Mult_Decomposition - (D1 => 0, - D2 => Big (Double_Uns'(Xhi * Yhi)), - D3 => Big (Double_Uns'(Xhi * Ylo)) + Big (Double_Uns'(Xlo * Yhi)) - + Big (Double_Uns (D (3))), - D4 => Big (Double_Uns (D (4))))); if Yhi /= 0 then T1 := Xlo * Yhi; Lemma_Hi_Lo (T1, Hi (T1), Lo (T1)); - pragma Assert - (Is_Mult_Decomposition - (D1 => 0, - D2 => Big (Double_Uns'(Xhi * Yhi)) + Big (Double_Uns (Hi (T1))), - D3 => Big (Double_Uns'(Xhi * Ylo)) + Big (Double_Uns (Lo (T1))) - + Big (Double_Uns (D (3))), - D4 => Big (Double_Uns (D (4))))); T2 := D (3) + Lo (T1); Lemma_Add_Commutation (Double_Uns (Lo (T1)), D (3)); - pragma Assert - (Is_Mult_Decomposition - (D1 => 0, - D2 => Big (Double_Uns'(Xhi * Yhi)) + Big (Double_Uns (Hi (T1))), - D3 => Big (Double_Uns'(Xhi * Ylo)) + Big (T2), - D4 => Big (Double_Uns (D (4))))); Lemma_Mult_Distribution (Big_2xxSingle, Big (Double_Uns (D (3))), Big (Double_Uns (Lo (T1)))); Lemma_Hi_Lo (T2, Hi (T2), Lo (T2)); - pragma Assert - (Is_Mult_Decomposition - (D1 => 0, - D2 => Big (Double_Uns'(Xhi * Yhi)) + Big (Double_Uns (Hi (T1))) - + Big (Double_Uns (Hi (T2))), - D3 => Big (Double_Uns'(Xhi * Ylo)) + Big (Double_Uns (Lo (T2))), - D4 => Big (Double_Uns (D (4))))); D (3) := Lo (T2); D (2) := Hi (T1) + Hi (T2); @@ -2639,30 +2536,11 @@ is pragma Assert (Big (Double_Uns (Hi (T1))) + Big (Double_Uns (Hi (T2))) = Big (Double_Uns (D (2)))); - pragma Assert - (Is_Mult_Decomposition - (D1 => 0, - D2 => Big (Double_Uns'(Xhi * Yhi)) + Big (Double_Uns (D (2))), - D3 => Big (Double_Uns'(Xhi * Ylo)) + Big (Double_Uns (D (3))), - D4 => Big (Double_Uns (D (4))))); if Xhi /= 0 then T1 := Xhi * Ylo; Lemma_Hi_Lo (T1, Hi (T1), Lo (T1)); - pragma Assert - (By (Is_Mult_Decomposition - (D1 => 0, - D2 => Big (Double_Uns'(Xhi * Yhi)) + Big (Double_Uns (D (2))) - + Big (Double_Uns (Hi (T1))), - D3 => Big (Double_Uns (Lo (T1))) + Big (Double_Uns (D (3))), - D4 => Big (Double_Uns (D (4)))), - (By (Big_2xxSingle * Big (T1) = - Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T1))) - + Big_2xxSingle * Big (Double_Uns (Lo (T1))), - Big_2xxSingle * Big (T1) = - Big_2xxSingle * (Big_2xxSingle * Big (Double_Uns (Hi (T1))) - + Big (Double_Uns (Lo (T1)))))))); T2 := D (3) + Lo (T1); @@ -2681,75 +2559,18 @@ is T3 := D (2) + Hi (T1); Lemma_Add_Commutation (Double_Uns (D (2)), Hi (T1)); - pragma Assert - (Is_Mult_Decomposition - (D1 => 0, - D2 => Big (Double_Uns'(Xhi * Yhi)) + Big (T3) - + Big (Double_Uns (Hi (T2))), - D3 => Big (Double_Uns (D (3))), - D4 => Big (Double_Uns (D (4))))); Lemma_Add_Commutation (T3, Hi (T2)); T3 := T3 + Hi (T2); T2 := Double_Uns'(Xhi * Yhi); - pragma Assert - (Is_Mult_Decomposition - (D1 => 0, - D2 => Big (T2) + Big (T3), - D3 => Big (Double_Uns (D (3))), - D4 => Big (Double_Uns (D (4))))); Lemma_Hi_Lo (T2, Hi (T2), Lo (T2)); - pragma Assert - (By (Is_Mult_Decomposition - (D1 => Big (Double_Uns (Hi (T2))), - D2 => Big (Double_Uns (Lo (T2))) + Big (T3), - D3 => Big (Double_Uns (D (3))), - D4 => Big (Double_Uns (D (4)))), - By (Big_2xxSingle * Big_2xxSingle * Big (T2) = - Big_2xxSingle * Big_2xxSingle * Big_2xxSingle - * Big (Double_Uns (Hi (T2))) - + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Lo (T2))), - Big_2xxSingle * Big_2xxSingle * - (Big_2xxSingle * Big (Double_Uns (Hi (T2))) - + Big (Double_Uns (Lo (T2)))) - = Big_2xxSingle * Big_2xxSingle * Big_2xxSingle - * Big (Double_Uns (Hi (T2))) - + Big_2xxSingle * Big_2xxSingle - * Big (Double_Uns (Lo (T2)))))); T1 := T3 + Lo (T2); D (2) := Lo (T1); Lemma_Add_Commutation (T3, Lo (T2)); - pragma Assert - (Is_Mult_Decomposition - (D1 => Big (Double_Uns (Hi (T2))), - D2 => Big (T1), - D3 => Big (Double_Uns (D (3))), - D4 => Big (Double_Uns (D (4))))); Lemma_Hi_Lo (T1, Hi (T1), Lo (T1)); - pragma Assert - (By (Is_Mult_Decomposition - (D1 => Big (Double_Uns (Hi (T2))) + Big (Double_Uns (Hi (T1))), - D2 => Big (Double_Uns (D (2))), - D3 => Big (Double_Uns (D (3))), - D4 => Big (Double_Uns (D (4)))), - By (Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Lo (T1))) = - Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2))), - D (2) = Lo (T1)) - and then - By (Big_2xxSingle * Big_2xxSingle * Big (T1) = - Big_2xxSingle * Big_2xxSingle * Big_2xxSingle - * Big (Double_Uns (Hi (T1))) - + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Lo (T1))), - Big_2xxSingle * Big_2xxSingle * - (Big_2xxSingle * Big (Double_Uns (Hi (T1))) - + Big (Double_Uns (Lo (T1)))) - = Big_2xxSingle * Big_2xxSingle * Big_2xxSingle - * Big (Double_Uns (Hi (T1))) - + Big_2xxSingle * Big_2xxSingle - * Big (Double_Uns (Lo (T1)))))); D (1) := Hi (T2) + Hi (T1); @@ -2759,75 +2580,42 @@ is pragma Assert (Big (Double_Uns (Hi (T2))) + Big (Double_Uns (Hi (T1))) = Big (Double_Uns (D (1)))); - pragma Assert - (By (Is_Mult_Decomposition - (D1 => Big (Double_Uns (D (1))), - D2 => Big (Double_Uns (D (2))), - D3 => Big (Double_Uns (D (3))), - D4 => Big (Double_Uns (D (4)))), - Big_2xxSingle * Big_2xxSingle * Big_2xxSingle * - Big (Double_Uns (D (1))) - = Big_2xxSingle * Big_2xxSingle * Big_2xxSingle * - (Big (Double_Uns (Hi (T2)) + Double_Uns (Hi (T1)))))); + (Is_Mult_Decomposition (D1 => Big (Double_Uns (D (1))), + D2 => Big (Double_Uns (D (2))), + D3 => Big (Double_Uns (D (3))), + D4 => Big (Double_Uns (D (4))))); else D (1) := 0; pragma Assert - (By (Is_Mult_Decomposition - (D1 => Big (Double_Uns (D (1))), - D2 => Big (Double_Uns (D (2))), - D3 => Big (Double_Uns (D (3))), - D4 => Big (Double_Uns (D (4)))), - Big (Double_Uns'(Xhi * Yhi)) = 0 - and then Big (Double_Uns'(Xhi * Ylo)) = 0 - and then Big (Double_Uns (D (1))) = 0)); + (Is_Mult_Decomposition (D1 => Big (Double_Uns (D (1))), + D2 => Big (Double_Uns (D (2))), + D3 => Big (Double_Uns (D (3))), + D4 => Big (Double_Uns (D (4))))); end if; - pragma Assert - (Is_Mult_Decomposition (D1 => Big (Double_Uns (D (1))), - D2 => Big (Double_Uns (D (2))), - D3 => Big (Double_Uns (D (3))), - D4 => Big (Double_Uns (D (4))))); else - pragma Assert - (By (Is_Mult_Decomposition - (D1 => 0, - D2 => 0, - D3 => Big (Double_Uns'(Xhi * Ylo)) + Big (Double_Uns (D (3))), - D4 => Big (Double_Uns (D (4)))), - Big (Double_Uns'(Xhi * Yhi)) = 0 - and then Big (Double_Uns'(Xlo * Yhi)) = 0)); - if Xhi /= 0 then T1 := Xhi * Ylo; Lemma_Hi_Lo (T1, Hi (T1), Lo (T1)); pragma Assert - (By (Is_Mult_Decomposition + (Is_Mult_Decomposition (D1 => 0, D2 => Big (Double_Uns (Hi (T1))), D3 => Big (Double_Uns (Lo (T1))) + Big (Double_Uns (D (3))), - D4 => Big (Double_Uns (D (4)))), - Big_2xxSingle * Big (Double_Uns'(Xhi * Ylo)) = - Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T1))) - + Big_2xxSingle * Big (Double_Uns (Lo (T1))))); + D4 => Big (Double_Uns (D (4))))); T2 := D (3) + Lo (T1); Lemma_Add_Commutation (Double_Uns (Lo (T1)), D (3)); pragma Assert - (By (Is_Mult_Decomposition + (Is_Mult_Decomposition (D1 => 0, D2 => Big (Double_Uns (Hi (T1))), D3 => Big (T2), - D4 => Big (Double_Uns (D (4)))), - Big_2xxSingle * Big (T2) = - Big_2xxSingle * - (Big (Double_Uns (Lo (T1))) + Big (Double_Uns (D (3)))))); - Lemma_Mult_Distribution (Big_2xxSingle, - Big (Double_Uns (D (3))), - Big (Double_Uns (Lo (T1)))); + D4 => Big (Double_Uns (D (4))))); Lemma_Hi_Lo (T2, Hi (T2), Lo (T2)); D (3) := Lo (T2); @@ -2849,22 +2637,42 @@ is D (2) := 0; pragma Assert - (By (Is_Mult_Decomposition + (Is_Mult_Decomposition (D1 => 0, D2 => Big (Double_Uns (D (2))), D3 => Big (Double_Uns (D (3))), - D4 => Big (Double_Uns (D (4)))), - Big (Double_Uns'(Xhi * Ylo)) = 0 - and then Big (Double_Uns (D (2))) = 0)); + D4 => Big (Double_Uns (D (4))))); end if; D (1) := 0; end if; - pragma Assert (Is_Mult_Decomposition (D1 => Big (Double_Uns (D (1))), - D2 => Big (Double_Uns (D (2))), - D3 => Big (Double_Uns (D (3))), - D4 => Big (Double_Uns (D (4))))); + pragma Assert_And_Cut + -- Restate the precondition + (Z /= 0 + and then In_Double_Int_Range + (if Round then Round_Quotient (Big (X) * Big (Y), Big (Z), + Big (X) * Big (Y) / Big (Z), + Big (X) * Big (Y) rem Big (Z)) + else Big (X) * Big (Y) / Big (Z)) + -- Restate the value of local variables + and then Zu = abs Z + and then Zhi = Hi (Zu) + and then Zlo = Lo (Zu) + and then Mult = abs (Big (X) * Big (Y)) + and then Quot = Big (X) * Big (Y) / Big (Z) + and then Big_R = Big (X) * Big (Y) rem Big (Z) + and then + (if Round then + Big_Q = Round_Quotient (Big (X) * Big (Y), Big (Z), Quot, Big_R) + else + Big_Q = Quot) + -- Summarize first part of the procedure + and then D'Initialized + and then Is_Mult_Decomposition (D1 => Big (Double_Uns (D (1))), + D2 => Big (Double_Uns (D (2))), + D3 => Big (Double_Uns (D (3))), + D4 => Big (Double_Uns (D (4))))); -- Now it is time for the dreaded multiple precision division. First an -- easy case, check for the simple case of a one digit divisor. @@ -2872,9 +2680,6 @@ is if Zhi = 0 then if D (1) /= 0 or else D (2) >= Zlo then if D (1) > 0 then - pragma Assert - (Mult >= Big_2xxSingle * Big_2xxSingle * Big_2xxSingle - * Big (Double_Uns (D (1)))); Lemma_Double_Big_2xxSingle; Lemma_Mult_Positive (Big_2xxDouble, Big_2xxSingle); Lemma_Ge_Mult (Big (Double_Uns (D (1))), @@ -2915,6 +2720,8 @@ is elsif (D (1) & D (2)) >= Zu then Lemma_Hi_Lo (D (1) & D (2), D (1), D (2)); Lemma_Ge_Commutation (D (1) & D (2), Zu); + pragma Assert + (Mult >= Big_2xxSingle * Big_2xxSingle * Big (D (1) & D (2))); Prove_Overflow; Raise_Error; @@ -2928,8 +2735,10 @@ is -- First normalize the divisor so that it has the leading bit on. -- We do this by finding the appropriate left shift amount. + Lemma_Hi_Lo (D (1) & D (2), D (1), D (2)); Lemma_Lt_Commutation (D (1) & D (2), Zu); - pragma Assert (Mult < Big_2xxDouble * Big (Zu)); + pragma Assert + (Mult < Big_2xxDouble * Big (Zu)); Shift := Single_Size; Mask := Single_Uns'Last; @@ -3127,7 +2936,8 @@ is Big (D (1) & D (2)), Big_2xxSingle * Big (Double_Uns (D (3))) + Big (Double_Uns (D (4)))); - pragma Assert (Big (D (1) & D (2)) < Big (Zu)); + pragma Assert + (Big (D (1) & D (2)) < Big (Zu)); -- Loop to compute quotient digits, runs twice for Qd (1) and Qd (2) @@ -3152,7 +2962,7 @@ is -- Local ghost variables Qd1 : Single_Uns := 0 with Ghost; - D234 : Big_Integer := 0 with Ghost; + D234 : Big_Integer with Ghost; D123 : constant Big_Integer := Big3 (D (1), D (2), D (3)) with Ghost; D4 : constant Big_Integer := Big (Double_Uns (D (4))) @@ -3160,11 +2970,10 @@ is begin Prove_Scaled_Mult_Decomposition_Regroup3 - (Big (Double_Uns (D (1))), - Big (Double_Uns (D (2))), - Big (Double_Uns (D (3))), - Big (Double_Uns (D (4)))); - pragma Assert (Mult * Big_2xx (Scale) = Big_2xxSingle * D123 + D4); + (D (1), D (2), D (3), D (4)); + pragma Assert + (By (Mult * Big_2xx (Scale) = Big_2xxSingle * D123 + D4, + Is_Scaled_Mult_Decomposition (0, 0, D123, D4))); for J in 1 .. 2 loop Lemma_Hi_Lo (D (J) & D (J + 1), D (J), D (J + 1)); @@ -3316,26 +3125,9 @@ is Lemma_Mult_Non_Negative (Big_2xxSingle, Big (Double_Uns (D (J + 1)))); pragma Assert - (By (Big3 (D (J), D (J + 1), D (J + 2)) >= + (Big3 (D (J), D (J + 1), D (J + 2)) >= Big_2xxSingle * Big_2xxSingle - * Big (Double_Uns (D (J))), - By (Big3 (D (J), D (J + 1), D (J + 2)) - - Big_2xxSingle * Big_2xxSingle - * Big (Double_Uns (D (J))) - = Big_2xxSingle * Big (Double_Uns (D (J + 1))) - + Big (Double_Uns (D (J + 2))), - Big3 (D (J), D (J + 1), D (J + 2)) = - Big_2xxSingle - * Big_2xxSingle * Big (Double_Uns (D (J))) - + Big_2xxSingle * Big (Double_Uns (D (J + 1))) - + Big (Double_Uns (D (J + 2)))) - and then - By (Big_2xxSingle * Big (Double_Uns (D (J + 1))) - + Big (Double_Uns (D (J + 2))) >= 0, - Big_2xxSingle * Big (Double_Uns (D (J + 1))) >= 0 - and then - Big (Double_Uns (D (J + 2))) >= 0 - ))); + * Big (Double_Uns (D (J)))); Lemma_Ge_Commutation (Double_Uns (D (J)), Double_Uns'(1)); Lemma_Ge_Mult (Big (Double_Uns (D (J))), Big (Double_Uns'(1)), @@ -3364,34 +3156,11 @@ is else pragma Assert (Qd1 = Qd (1)); pragma Assert - (By (Mult * Big_2xx (Scale) = - Big_2xxSingle * Big (Double_Uns (Qd1)) * Big (Zu) - + Big3 (S1, S2, S3) - + Big3 (D (2), D (3), D (4)), - Big3 (D (2), D (3), D (4)) = D234 - Big3 (S1, S2, S3))); - pragma Assert - (By (Mult * Big_2xx (Scale) = + (Mult * Big_2xx (Scale) = Big_2xxSingle * Big (Double_Uns (Qd (1))) * Big (Zu) + Big (Double_Uns (Qd (2))) * Big (Zu) + Big_2xxSingle * Big (Double_Uns (D (3))) - + Big (Double_Uns (D (4))), - Big_2xxSingle * Big (Double_Uns (Qd (1))) * Big (Zu) - = Big_2xxSingle * Big (Double_Uns (Qd1)) * Big (Zu) - and then - Big3 (S1, S2, S3) = Big (Double_Uns (Qd (2))) * Big (Zu) - and then - By (Big3 (D (2), D (3), D (4)) - = Big_2xxSingle * Big (Double_Uns (D (3))) - + Big (Double_Uns (D (4))), - Big3 (D (2), D (3), D (4)) - = Big_2xxSingle * Big_2xxSingle * - Big (Double_Uns (D (2))) - + Big_2xxSingle * Big (Double_Uns (D (3))) - + Big (Double_Uns (D (4))) - and then - Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2))) - = 0) - )); + + Big (Double_Uns (D (4)))); end if; end loop; end; @@ -3543,12 +3312,6 @@ is Lemma_Add_Commutation (Double_Uns (X1), Y1); Lemma_Add_Commutation (Double_Uns (X2), Y2); Lemma_Add_Commutation (Double_Uns (X3), Y3); - pragma Assert (Double_Uns (Single_Uns'(X1 + Y1)) - = Double_Uns (X1) + Double_Uns (Y1)); - pragma Assert (Double_Uns (Single_Uns'(X2 + Y2)) - = Double_Uns (X2) + Double_Uns (Y2)); - pragma Assert (Double_Uns (Single_Uns'(X3 + Y3)) - = Double_Uns (X3) + Double_Uns (Y3)); end Lemma_Add3_No_Carry; --------------------- diff --git a/gcc/ada/libgnat/s-aridou.ads b/gcc/ada/libgnat/s-aridou.ads index 58aa775..b22f0db 100644 --- a/gcc/ada/libgnat/s-aridou.ads +++ b/gcc/ada/libgnat/s-aridou.ads @@ -77,18 +77,24 @@ is function Big (Arg : Double_Int) return Big_Integer is (Signed_Conversion.To_Big_Integer (Arg)) - with Ghost; + with + Ghost, + Annotate => (GNATprove, Inline_For_Proof); package Unsigned_Conversion is new BI_Ghost.Unsigned_Conversions (Int => Double_Uns); function Big (Arg : Double_Uns) return Big_Integer is (Unsigned_Conversion.To_Big_Integer (Arg)) - with Ghost; + with + Ghost, + Annotate => (GNATprove, Inline_For_Proof); function In_Double_Int_Range (Arg : Big_Integer) return Boolean is (BI_Ghost.In_Range (Arg, Big (Double_Int'First), Big (Double_Int'Last))) - with Ghost; + with + Ghost, + Annotate => (GNATprove, Inline_For_Proof); function Add_With_Ovflo_Check (X, Y : Double_Int) return Double_Int with diff --git a/gcc/ada/libgnat/s-arit32.adb b/gcc/ada/libgnat/s-arit32.adb index bd316c1..d19b9e1 100644 --- a/gcc/ada/libgnat/s-arit32.adb +++ b/gcc/ada/libgnat/s-arit32.adb @@ -104,9 +104,8 @@ is function To_Neg_Int (A : Uns32) return Int32 with - Annotate => (GNATprove, Always_Return), - Pre => In_Int32_Range (-Big (A)), - Post => Big (To_Neg_Int'Result) = -Big (A); + Pre => In_Int32_Range (-Big (A)), + Post => Big (To_Neg_Int'Result) = -Big (A); -- Convert to negative integer equivalent. If the input is in the range -- 0 .. 2**31, then the corresponding nonpositive signed integer (obtained -- by negating the given value) is returned, otherwise constraint error is @@ -114,9 +113,8 @@ is function To_Pos_Int (A : Uns32) return Int32 with - Annotate => (GNATprove, Always_Return), - Pre => In_Int32_Range (Big (A)), - Post => Big (To_Pos_Int'Result) = Big (A); + Pre => In_Int32_Range (Big (A)), + Post => Big (To_Pos_Int'Result) = Big (A); -- Convert to positive integer equivalent. If the input is in the range -- 0 .. 2**31 - 1, then the corresponding nonnegative signed integer is -- returned, otherwise constraint error is raised. @@ -195,12 +193,6 @@ is or else (X >= Big_0 and then Y <= Big_0), Post => X * Y <= Big_0; - procedure Lemma_Neg_Div (X, Y : Big_Integer) - with - Ghost, - Pre => Y /= 0, - Post => X / Y = (-X) / (-Y); - procedure Lemma_Neg_Rem (X, Y : Big_Integer) with Ghost, @@ -223,6 +215,7 @@ is ----------------------------- procedure Lemma_Abs_Commutation (X : Int32) is null; + procedure Lemma_Abs_Div_Commutation (X, Y : Big_Integer) is null; procedure Lemma_Abs_Mult_Commutation (X, Y : Big_Integer) is null; procedure Lemma_Div_Commutation (X, Y : Uns64) is null; procedure Lemma_Div_Ge (X, Y, Z : Big_Integer) is null; @@ -235,22 +228,6 @@ is procedure Lemma_Rem_Commutation (X, Y : Uns64) is null; ------------------------------- - -- Lemma_Abs_Div_Commutation -- - ------------------------------- - - procedure Lemma_Abs_Div_Commutation (X, Y : Big_Integer) is - begin - if Y < 0 then - if X < 0 then - pragma Assert (abs (X / Y) = abs (X / (-Y))); - else - Lemma_Neg_Div (X, Y); - pragma Assert (abs (X / Y) = abs ((-X) / (-Y))); - end if; - end if; - end Lemma_Abs_Div_Commutation; - - ------------------------------- -- Lemma_Abs_Rem_Commutation -- ------------------------------- @@ -277,16 +254,6 @@ is pragma Assert (Uns64 (Xlo) = Xu mod 2 ** 32); end Lemma_Hi_Lo; - ------------------- - -- Lemma_Neg_Div -- - ------------------- - - procedure Lemma_Neg_Div (X, Y : Big_Integer) is - begin - pragma Assert ((-X) / (-Y) = -(X / (-Y))); - pragma Assert (X / (-Y) = -(X / Y)); - end Lemma_Neg_Div; - ----------------- -- Raise_Error -- ----------------- diff --git a/gcc/ada/libgnat/s-atacco.adb b/gcc/ada/libgnat/s-atacco.adb index a98b25c..8c10681 100644 --- a/gcc/ada/libgnat/s-atacco.adb +++ b/gcc/ada/libgnat/s-atacco.adb @@ -29,8 +29,8 @@ -- -- ------------------------------------------------------------------------------ --- This package does not require a body, since it is a package renaming. We --- provide a dummy file containing a No_Body pragma so that previous versions --- of the body (which did exist) will not interfere. +-- This package does not require a body. We provide a dummy file containing a +-- No_Body pragma so that previous versions of the body (which did exist) will +-- not interfere. pragma No_Body; diff --git a/gcc/ada/libgnat/s-atacco.ads b/gcc/ada/libgnat/s-atacco.ads index bd920cc..157ca52 100644 --- a/gcc/ada/libgnat/s-atacco.ads +++ b/gcc/ada/libgnat/s-atacco.ads @@ -55,11 +55,9 @@ package System.Address_To_Access_Conversions is -- of no strict aliasing. function To_Pointer (Value : Address) return Object_Pointer with - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; function To_Address (Value : Object_Pointer) return Address with - SPARK_Mode => Off, - Annotate => (GNATprove, Always_Return); + SPARK_Mode => Off; pragma Import (Intrinsic, To_Pointer); pragma Import (Intrinsic, To_Address); diff --git a/gcc/ada/libgnat/s-atopri__32.ads b/gcc/ada/libgnat/s-atopri__32.ads new file mode 100644 index 0000000..1281e9b --- /dev/null +++ b/gcc/ada/libgnat/s-atopri__32.ads @@ -0,0 +1,149 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT RUN-TIME COMPONENTS -- +-- -- +-- S Y S T E M . A T O M I C _ P R I M I T I V E S -- +-- -- +-- S p e c -- +-- -- +-- Copyright (C) 2012-2023, 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 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. +-- This is the version that only contains primitives available on 32 bit +-- platforms. + +with Interfaces.C; + +package System.Atomic_Primitives is + pragma Pure; + + type uint is mod 2 ** Long_Integer'Size; + + type uint8 is mod 2**8 + with Size => 8; + + type uint16 is mod 2**16 + with Size => 16; + + type uint32 is mod 2**32 + with Size => 32; + + Relaxed : constant := 0; + Consume : constant := 1; + Acquire : constant := 2; + Release : constant := 3; + Acq_Rel : constant := 4; + Seq_Cst : constant := 5; + Last : constant := 6; + + subtype Mem_Model is Integer range Relaxed .. Last; + + ------------------------------------ + -- GCC built-in atomic primitives -- + ------------------------------------ + + generic + type Atomic_Type is mod <>; + function Atomic_Load + (Ptr : Address; + Model : Mem_Model := Seq_Cst) return Atomic_Type; + pragma Import (Intrinsic, Atomic_Load, "__atomic_load_n"); + + 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); + + generic + type Atomic_Type is mod <>; + function Atomic_Compare_Exchange + (Ptr : Address; + Expected : 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, "__atomic_compare_exchange_n"); + + function Atomic_Compare_Exchange_8 is new Atomic_Compare_Exchange (uint8); + function Atomic_Compare_Exchange_16 is new Atomic_Compare_Exchange (uint16); + function Atomic_Compare_Exchange_32 is new Atomic_Compare_Exchange (uint32); + + function Atomic_Test_And_Set + (Ptr : System.Address; + Model : Mem_Model := Seq_Cst) return Boolean; + pragma Import (Intrinsic, Atomic_Test_And_Set, "__atomic_test_and_set"); + + procedure Atomic_Clear + (Ptr : System.Address; + Model : Mem_Model := Seq_Cst); + pragma Import (Intrinsic, Atomic_Clear, "__atomic_clear"); + + function Atomic_Always_Lock_Free + (Size : Interfaces.C.size_t; + Ptr : System.Address := System.Null_Address) return Boolean; + pragma Import + (Intrinsic, Atomic_Always_Lock_Free, "__atomic_always_lock_free"); + + -------------------------- + -- Lock-free operations -- + -------------------------- + + -- The lock-free implementation uses two atomic instructions for the + -- expansion of protected operations: + + -- * Lock_Free_Read atomically loads the value contained in Ptr (with the + -- Acquire synchronization mode). + + -- * 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. + + generic + type Atomic_Type is mod <>; + function Lock_Free_Read (Ptr : Address) return Atomic_Type; + + 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); + + 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_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); + +private + pragma Inline (Lock_Free_Read); + pragma Inline (Lock_Free_Try_Write); +end System.Atomic_Primitives; diff --git a/gcc/ada/libgnat/s-bituti.adb b/gcc/ada/libgnat/s-bituti.adb index 1b0acc1..28e41f3 100644 --- a/gcc/ada/libgnat/s-bituti.adb +++ b/gcc/ada/libgnat/s-bituti.adb @@ -29,11 +29,13 @@ -- -- ------------------------------------------------------------------------------ +with System.Storage_Elements; use System.Storage_Elements; + package body System.Bitfield_Utils is package body G is - Val_Bytes : constant Address := Address (Val'Size / Storage_Unit); + Val_Bytes : constant Storage_Count := Val'Size / Storage_Unit; -- A Val_2 can cross a memory page boundary (e.g. an 8-byte Val_2 that -- starts 4 bytes before the end of a page). If the bit field also @@ -119,7 +121,7 @@ package body System.Bitfield_Utils is Size : Small_Size) return Val_2 is begin - pragma Assert (Src_Address mod Val'Alignment = 0); + pragma Assert (Src_Address mod Storage_Count'(Val'Alignment) = 0); -- Bit field fits in first half; fetch just one Val. On little -- endian, we want that in the low half, but on big endian, we @@ -154,7 +156,7 @@ package body System.Bitfield_Utils is V : Val_2; Size : Small_Size) is begin - pragma Assert (Dest_Address mod Val'Alignment = 0); + pragma Assert (Dest_Address mod Storage_Count'(Val'Alignment) = 0); -- Comments in Get_Val_2 apply, except we're storing instead of -- fetching. @@ -381,18 +383,19 @@ package body System.Bitfield_Utils is -- Align the Address values as for Val and Val_2, and adjust the -- Bit_Offsets accordingly. - Src_Adjust : constant Address := Src_Address mod Val_Bytes; + Src_Adjust : constant Storage_Offset := Src_Address mod Val_Bytes; Al_Src_Address : constant Address := Src_Address - Src_Adjust; Al_Src_Offset : constant Bit_Offset := Src_Offset + Bit_Offset (Src_Adjust * Storage_Unit); - Dest_Adjust : constant Address := Dest_Address mod Val_Bytes; + Dest_Adjust : constant Storage_Offset := + Dest_Address mod Val_Bytes; Al_Dest_Address : constant Address := Dest_Address - Dest_Adjust; Al_Dest_Offset : constant Bit_Offset := Dest_Offset + Bit_Offset (Dest_Adjust * Storage_Unit); - pragma Assert (Al_Src_Address mod Val'Alignment = 0); - pragma Assert (Al_Dest_Address mod Val'Alignment = 0); + pragma Assert (Al_Src_Address mod Storage_Count'(Val'Alignment) = 0); + pragma Assert (Al_Dest_Address mod Storage_Count'(Val'Alignment) = 0); begin -- Optimized small case diff --git a/gcc/ada/libgnat/s-carun8.adb b/gcc/ada/libgnat/s-carun8.adb index 3a88a9c..b0f2d94b 100644 --- a/gcc/ada/libgnat/s-carun8.adb +++ b/gcc/ada/libgnat/s-carun8.adb @@ -72,7 +72,7 @@ package body System.Compare_Array_Unsigned_8 is begin -- If operands are non-aligned, or length is too short, go by bytes - if (ModA (OrA (Left, Right), 4) /= 0) or else Compare_Len < 4 then + if ModA (OrA (Left, Right), 4) /= 0 or else Compare_Len < 4 then return Compare_Array_U8_Unaligned (Left, Right, Left_Len, Right_Len); end if; diff --git a/gcc/ada/libgnat/s-crtl.ads b/gcc/ada/libgnat/s-crtl.ads index 4b6fc76..c3a3b64 100644 --- a/gcc/ada/libgnat/s-crtl.ads +++ b/gcc/ada/libgnat/s-crtl.ads @@ -55,10 +55,9 @@ package System.CRTL is subtype off_t is Long_Integer; - type size_t is mod 2 ** Standard'Address_Size; + type size_t is mod System.Memory_Size; - type ssize_t is range -(2 ** (Standard'Address_Size - 1)) - .. +(2 ** (Standard'Address_Size - 1)) - 1; + type ssize_t is range -Memory_Size / 2 .. Memory_Size / 2 - 1; type int64 is new Long_Long_Integer; -- Note: we use Long_Long_Integer'First instead of -2 ** 63 to allow this diff --git a/gcc/ada/libgnat/s-dwalin.adb b/gcc/ada/libgnat/s-dwalin.adb index d38bc05..d35d03a 100644 --- a/gcc/ada/libgnat/s-dwalin.adb +++ b/gcc/ada/libgnat/s-dwalin.adb @@ -1542,7 +1542,7 @@ package body System.Dwarf_Lines is exit when Ar_Start = Null_Address and Ar_Len = 0; Len := uint32 (Ar_Len); - Start := uint32 (Address'(Ar_Start - C.Low)); + Start := uint32 (Storage_Count'(Ar_Start - C.Low)); -- Search START in the array @@ -1762,7 +1762,7 @@ package body System.Dwarf_Lines is if C.Cache /= null then declare - Addr_Off : constant uint32 := uint32 (Address'(Addr - C.Low)); + Off : constant uint32 := uint32 (Storage_Count'(Addr - C.Low)); First, Last, Mid : Natural; begin @@ -1772,17 +1772,17 @@ package body System.Dwarf_Lines is while First <= Last loop Mid := First + (Last - First) / 2; - if Addr_Off < C.Cache (Mid).First then + if Off < C.Cache (Mid).First then Last := Mid - 1; - elsif Addr_Off >= C.Cache (Mid).First + C.Cache (Mid).Size then + elsif Off >= C.Cache (Mid).First + C.Cache (Mid).Size then First := Mid + 1; else exit; end if; end loop; - if Addr_Off >= C.Cache (Mid).First - and then Addr_Off < C.Cache (Mid).First + C.Cache (Mid).Size + if Off >= C.Cache (Mid).First + and then Off < C.Cache (Mid).First + C.Cache (Mid).Size then Line_Offset := Offset (C.Cache (Mid).Line); S := Read_Symbol (C.Obj.all, Offset (C.Cache (Mid).Sym)); diff --git a/gcc/ada/libgnat/s-expmod.adb b/gcc/ada/libgnat/s-expmod.adb index 6cf68a5..aa6e9b4 100644 --- a/gcc/ada/libgnat/s-expmod.adb +++ b/gcc/ada/libgnat/s-expmod.adb @@ -109,9 +109,21 @@ is procedure Lemma_Euclidean_Mod (Q, F, R : Big_Natural) with Pre => F /= 0, - Post => (Q * F + R) mod F = R mod F; + Post => (Q * F + R) mod F = R mod F, + Subprogram_Variant => (Decreases => Q); - procedure Lemma_Euclidean_Mod (Q, F, R : Big_Natural) is null; + ------------------------- + -- Lemma_Euclidean_Mod -- + ------------------------- + + procedure Lemma_Euclidean_Mod (Q, F, R : Big_Natural) is + begin + if Q > 0 then + Lemma_Euclidean_Mod (Q - 1, F, R); + end if; + end Lemma_Euclidean_Mod; + + -- Local variables Left : constant Big_Natural := (X + Y) mod B; Right : constant Big_Natural := ((X mod B) + (Y mod B)) mod B; @@ -164,6 +176,9 @@ is Lemma_Mod_Mod (A, B); Lemma_Exp_Mod (A, Exp - 1, B); Lemma_Mult_Mod (A, A ** (Exp - 1), B); + pragma Assert + ((A mod B) * (A mod B) ** (Exp - 1) = (A mod B) ** Exp); + pragma Assert (A * A ** (Exp - 1) = A ** Exp); pragma Assert (Left = Right); end; end if; @@ -190,6 +205,7 @@ is pragma Assert (Left = Right); else pragma Assert (Y mod B = 0); + pragma Assert (Y / B * B = Y); pragma Assert ((X * Y) mod B = (X * Y) - (X * Y) / B * B); pragma Assert ((X * Y) mod B = (X * Y) - (X * (Y / B) * B) / B * B); @@ -309,6 +325,7 @@ is Lemma_Mod_Mod (Rest * Rest, Big (Modulus)); Lemma_Mod_Ident (Big (Result), Big (Modulus)); Lemma_Mult_Mod (Big (Result), Rest * Rest, Big (Modulus)); + pragma Assert (Big (Factor) >= 0); Lemma_Mult_Mod (Big (Result), Big (Factor) ** Exp, Big (Modulus)); pragma Assert (Equal_Modulo diff --git a/gcc/ada/libgnat/s-genbig.adb b/gcc/ada/libgnat/s-genbig.adb index 85dc40b..e1f2e5c 100644 --- a/gcc/ada/libgnat/s-genbig.adb +++ b/gcc/ada/libgnat/s-genbig.adb @@ -49,6 +49,10 @@ package body System.Generic_Bignums is -- Compose double digit value from two single digit values subtype LLI is Long_Long_Integer; + subtype LLLI is Long_Long_Long_Integer; + + LLLI_Is_128 : constant Boolean := Long_Long_Long_Integer'Size = 128; + -- True if Long_Long_Long_Integer is 128-bit large One_Data : constant Digit_Vector (1 .. 1) := [1]; -- Constant one @@ -318,7 +322,7 @@ package body System.Generic_Bignums is elsif X.Len = 1 and then X.D (1) = 1 then return Normalize - (X.D, Neg => X.Neg and then ((Y.D (Y.Len) and 1) = 1)); + (X.D, Neg => X.Neg and then (Y.D (Y.Len) and 1) = 1); -- If the absolute value of the base is greater than 1, then the -- exponent must not be bigger than one word, otherwise the result @@ -694,14 +698,14 @@ package body System.Generic_Bignums is -- Lengths are different, that's decisive since no leading zeroes elsif X'Last /= Y'Last then - return (if (X'Last > Y'Last) xor X_Neg then GT else LT); + return (if X'Last > Y'Last xor X_Neg then GT else LT); -- Need to compare data else for J in X'Range loop if X (J) /= Y (J) then - return (if (X (J) > Y (J)) xor X_Neg then GT else LT); + return (if X (J) > Y (J) xor X_Neg then GT else LT); end if; end loop; @@ -1041,22 +1045,48 @@ package body System.Generic_Bignums is -- From_Bignum -- ----------------- - function From_Bignum (X : Bignum) return Long_Long_Integer is + function From_Bignum (X : Bignum) return Long_Long_Long_Integer is begin if X.Len = 0 then return 0; elsif X.Len = 1 then - return (if X.Neg then -LLI (X.D (1)) else LLI (X.D (1))); + return (if X.Neg then -LLLI (X.D (1)) else LLLI (X.D (1))); elsif X.Len = 2 then declare Mag : constant DD := X.D (1) & X.D (2); begin - if X.Neg and then Mag <= 2 ** 63 then - return -LLI (Mag); - elsif Mag < 2 ** 63 then - return LLI (Mag); + if X.Neg and then (Mag <= 2 ** 63 or else LLLI_Is_128) then + return -LLLI (Mag); + elsif Mag < 2 ** 63 or else LLLI_Is_128 then + return LLLI (Mag); + end if; + end; + + elsif X.Len = 3 and then LLLI_Is_128 then + declare + Hi : constant SD := X.D (1); + Lo : constant DD := X.D (2) & X.D (3); + Mag : constant Unsigned_128 := + Shift_Left (Unsigned_128 (Hi), 64) + Unsigned_128 (Lo); + begin + return (if X.Neg then -LLLI (Mag) else LLLI (Mag)); + end; + + elsif X.Len = 4 and then LLLI_Is_128 then + declare + Hi : constant DD := X.D (1) & X.D (2); + Lo : constant DD := X.D (3) & X.D (4); + Mag : constant Unsigned_128 := + Shift_Left (Unsigned_128 (Hi), 64) + Unsigned_128 (Lo); + begin + if X.Neg + and then (Hi < 2 ** 63 or else (Hi = 2 ** 63 and then Lo = 0)) + then + return -LLLI (Mag); + elsif Hi < 2 ** 63 then + return LLLI (Mag); end if; end; end if; @@ -1064,6 +1094,44 @@ package body System.Generic_Bignums is raise Constraint_Error with "expression value out of range"; end From_Bignum; + function From_Bignum (X : Bignum) return Long_Long_Integer is + begin + return Long_Long_Integer (Long_Long_Long_Integer'(From_Bignum (X))); + end From_Bignum; + + function From_Bignum (X : Bignum) return Unsigned_128 is + begin + if X.Neg then + null; + + elsif X.Len = 0 then + return 0; + + elsif X.Len = 1 then + return Unsigned_128 (X.D (1)); + + elsif X.Len = 2 then + return Unsigned_128 (DD'(X.D (1) & X.D (2))); + + elsif X.Len = 3 and then LLLI_Is_128 then + return + Shift_Left (Unsigned_128 (X.D (1)), 64) + + Unsigned_128 (DD'(X.D (2) & X.D (3))); + + elsif X.Len = 4 and then LLLI_Is_128 then + return + Shift_Left (Unsigned_128 (DD'(X.D (1) & X.D (2))), 64) + + Unsigned_128 (DD'(X.D (3) & X.D (4))); + end if; + + raise Constraint_Error with "expression value out of range"; + end From_Bignum; + + function From_Bignum (X : Bignum) return Unsigned_64 is + begin + return Unsigned_64 (Unsigned_128'(From_Bignum (X))); + end From_Bignum; + ------------------------- -- Bignum_In_LLI_Range -- ------------------------- @@ -1161,29 +1229,27 @@ package body System.Generic_Bignums is elsif X = -2 ** 63 then return Allocate_Big_Integer ([2 ** 31, 0], True); - elsif Long_Long_Long_Integer'Size = 128 - and then X = Long_Long_Long_Integer'First - then + elsif LLLI_Is_128 and then X = Long_Long_Long_Integer'First then return Allocate_Big_Integer ([2 ** 31, 0, 0, 0], True); -- Other negative numbers elsif X < 0 then - if Long_Long_Long_Integer'Size = 64 then + if LLLI_Is_128 then + return Convert_128 (-X, True); + else return Allocate_Big_Integer ((SD ((-X) / Base), SD ((-X) mod Base)), True); - else - return Convert_128 (-X, True); end if; -- Positive numbers else - if Long_Long_Long_Integer'Size = 64 then + if LLLI_Is_128 then + return Convert_128 (X, False); + else return Allocate_Big_Integer ((SD (X / Base), SD (X mod Base)), False); - else - return Convert_128 (X, False); end if; end if; end To_Bignum; @@ -1285,7 +1351,7 @@ package body System.Generic_Bignums is function Image (Arg : Bignum) return String is begin if Big_LT (Arg, Big_Base'Unchecked_Access) then - return [Hex_Chars (Natural (From_Bignum (Arg)))]; + return [Hex_Chars (Natural (LLI'(From_Bignum (Arg))))]; else declare Div : aliased Big_Integer; @@ -1294,7 +1360,7 @@ package body System.Generic_Bignums is begin Div_Rem (Arg, Big_Base'Unchecked_Access, Div, Remain); - R := Natural (From_Bignum (To_Bignum (Remain))); + R := Natural (LLI'(From_Bignum (To_Bignum (Remain)))); Free_Big_Integer (Remain); return S : constant String := diff --git a/gcc/ada/libgnat/s-genbig.ads b/gcc/ada/libgnat/s-genbig.ads index 9cf944c..167f24f 100644 --- a/gcc/ada/libgnat/s-genbig.ads +++ b/gcc/ada/libgnat/s-genbig.ads @@ -117,6 +117,18 @@ package System.Generic_Bignums is -- Convert Bignum to Long_Long_Integer. Constraint_Error raised with -- appropriate message if value is out of range of Long_Long_Integer. + function From_Bignum (X : Bignum) return Long_Long_Long_Integer; + -- Convert Bignum to Long_Long_Long_Integer. Constraint_Error raised with + -- appropriate message if value is out of range of Long_Long_Long_Integer. + + function From_Bignum (X : Bignum) return Interfaces.Unsigned_64; + -- Convert Bignum to Unsigned_64. Constraint_Error raised with + -- appropriate message if value is out of range of Unsigned_64. + + function From_Bignum (X : Bignum) return Interfaces.Unsigned_128; + -- Convert Bignum to Unsigned_128. Constraint_Error raised with + -- appropriate message if value is out of range of Unsigned_128. + function To_String (X : Bignum; Width : Natural := 0; Base : Positive := 10) return String; diff --git a/gcc/ada/libgnat/s-memory.ads b/gcc/ada/libgnat/s-memory.ads index dc431b7..4f6dd3d2 100644 --- a/gcc/ada/libgnat/s-memory.ads +++ b/gcc/ada/libgnat/s-memory.ads @@ -43,7 +43,7 @@ package System.Memory is pragma Elaborate_Body; - type size_t is mod 2 ** Standard'Address_Size; + type size_t is mod Memory_Size; -- Note: the reason we redefine this here instead of using the -- definition in Interfaces.C is that we do not want to drag in -- all of Interfaces.C just because System.Memory is used. diff --git a/gcc/ada/libgnat/s-mmap.adb b/gcc/ada/libgnat/s-mmap.adb index ed4c2bd..abb870e 100644 --- a/gcc/ada/libgnat/s-mmap.adb +++ b/gcc/ada/libgnat/s-mmap.adb @@ -75,7 +75,7 @@ package body System.Mmap is -- Whether this region is actually memory mapped Mutable : Boolean; - -- If the file is opened for reading, wheter this region is writable + -- If the file is opened for reading, whether this region is writable Buffer : System.Strings.String_Access; -- When this region is not actually memory mapped, contains the @@ -284,9 +284,8 @@ package body System.Mmap is if (File.File.Write or else Region.Mutable = Mutable) and then Req_Offset >= Region.System_Offset - and then - (Req_Offset + Req_Length - <= Region.System_Offset + Region.System_Size) + and then Req_Offset + Req_Length <= + Region.System_Offset + Region.System_Size then Region.User_Offset := Req_Offset; Compute_Data (Region); diff --git a/gcc/ada/libgnat/s-parame.adb b/gcc/ada/libgnat/s-parame.adb index 930c92d..6bd9f03 100644 --- a/gcc/ada/libgnat/s-parame.adb +++ b/gcc/ada/libgnat/s-parame.adb @@ -58,6 +58,8 @@ package body System.Parameters is begin if Default_Stack_Size = -1 then return 2 * 1024 * 1024; + elsif Size_Type (Default_Stack_Size) < Minimum_Stack_Size then + return Minimum_Stack_Size; else return Size_Type (Default_Stack_Size); end if; diff --git a/gcc/ada/libgnat/s-parame.ads b/gcc/ada/libgnat/s-parame.ads index 3d6e345..72e7238 100644 --- a/gcc/ada/libgnat/s-parame.ads +++ b/gcc/ada/libgnat/s-parame.ads @@ -53,9 +53,7 @@ package System.Parameters is -- Task And Stack Allocation Control -- --------------------------------------- - type Size_Type is range - -(2 ** (Integer'(Standard'Address_Size) - 1)) .. - +(2 ** (Integer'(Standard'Address_Size) - 1)) - 1; + type Size_Type is range -Memory_Size / 2 .. Memory_Size / 2 - 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 diff --git a/gcc/ada/libgnat/s-parame__hpux.ads b/gcc/ada/libgnat/s-parame__hpux.ads index 542131f..243f8c3 100644 --- a/gcc/ada/libgnat/s-parame__hpux.ads +++ b/gcc/ada/libgnat/s-parame__hpux.ads @@ -53,9 +53,7 @@ package System.Parameters is -- Task And Stack Allocation Control -- --------------------------------------- - type Size_Type is range - -(2 ** (Integer'(Standard'Address_Size) - 1)) .. - +(2 ** (Integer'(Standard'Address_Size) - 1)) - 1; + type Size_Type is range -Memory_Size / 2 .. Memory_Size / 2 - 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 diff --git a/gcc/ada/libgnat/s-parame__posix2008.ads b/gcc/ada/libgnat/s-parame__posix2008.ads index 4f5d47a..16555e1 100644 --- a/gcc/ada/libgnat/s-parame__posix2008.ads +++ b/gcc/ada/libgnat/s-parame__posix2008.ads @@ -53,9 +53,7 @@ package System.Parameters is -- Task And Stack Allocation Control -- --------------------------------------- - type Size_Type is range - -(2 ** (Integer'(Standard'Address_Size) - 1)) .. - +(2 ** (Integer'(Standard'Address_Size) - 1)) - 1; + type Size_Type is range -Memory_Size / 2 .. Memory_Size / 2 - 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 diff --git a/gcc/ada/libgnat/s-parame__qnx.adb b/gcc/ada/libgnat/s-parame__qnx.adb new file mode 100644 index 0000000..d9b46b6 --- /dev/null +++ b/gcc/ada/libgnat/s-parame__qnx.adb @@ -0,0 +1,81 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT COMPILER COMPONENTS -- +-- -- +-- S Y S T E M . P A R A M E T E R S -- +-- -- +-- B o d y -- +-- -- +-- Copyright (C) 1995-2023, 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 version for AArch64 QNX + +package body System.Parameters is + + ------------------------- + -- Adjust_Storage_Size -- + ------------------------- + + function Adjust_Storage_Size (Size : Size_Type) return Size_Type is + begin + if Size = Unspecified_Size then + return Default_Stack_Size; + elsif Size < Minimum_Stack_Size then + return Minimum_Stack_Size; + else + return Size; + end if; + end Adjust_Storage_Size; + + ------------------------ + -- Default_Stack_Size -- + ------------------------ + + function Default_Stack_Size return Size_Type is + Default_Stack_Size : constant Integer; + pragma Import (C, Default_Stack_Size, "__gl_default_stack_size"); + begin + if Default_Stack_Size = -1 then + -- 256K is the default stack size on aarch64 QNX + return 256 * 1024; + elsif Size_Type (Default_Stack_Size) < Minimum_Stack_Size then + return Minimum_Stack_Size; + else + return Size_Type (Default_Stack_Size); + end if; + end Default_Stack_Size; + + ------------------------ + -- Minimum_Stack_Size -- + ------------------------ + + function Minimum_Stack_Size return Size_Type is + begin + -- 256 is the value of PTHREAD_STACK_MIN on QNX and + -- 12K is required for stack-checking. The value is + -- rounded up to a multiple of a 4K page. + return 16 * 1024; + end Minimum_Stack_Size; + +end System.Parameters; diff --git a/gcc/ada/libgnat/s-parame__rtems.adb b/gcc/ada/libgnat/s-parame__rtems.adb index 2f2e70b..1d51ae9 100644 --- a/gcc/ada/libgnat/s-parame__rtems.adb +++ b/gcc/ada/libgnat/s-parame__rtems.adb @@ -63,6 +63,8 @@ package body System.Parameters is begin if Default_Stack_Size = -1 then return 32 * 1024; + elsif Size_Type (Default_Stack_Size) < Minimum_Stack_Size then + return Minimum_Stack_Size; else return Size_Type (Default_Stack_Size); end if; diff --git a/gcc/ada/libgnat/s-parame__vxworks.adb b/gcc/ada/libgnat/s-parame__vxworks.adb index 8e0768e..38fe022 100644 --- a/gcc/ada/libgnat/s-parame__vxworks.adb +++ b/gcc/ada/libgnat/s-parame__vxworks.adb @@ -58,11 +58,13 @@ package body System.Parameters is begin if Default_Stack_Size = -1 then if Stack_Check_Limits then - return 32 * 1024; -- Extra stack to allow for 12K exception area. + return 32 * 1024; else return 20 * 1024; end if; + elsif Size_Type (Default_Stack_Size) < Minimum_Stack_Size then + return Minimum_Stack_Size; else return Size_Type (Default_Stack_Size); end if; @@ -74,7 +76,12 @@ package body System.Parameters is function Minimum_Stack_Size return Size_Type is begin - return 8 * 1024; + if Stack_Check_Limits then + -- Extra stack to allow for 12K exception area. + return 20 * 1024; + else + return 8 * 1024; + end if; end Minimum_Stack_Size; end System.Parameters; diff --git a/gcc/ada/libgnat/s-parame__vxworks.ads b/gcc/ada/libgnat/s-parame__vxworks.ads index adae27d..6cf32ca 100644 --- a/gcc/ada/libgnat/s-parame__vxworks.ads +++ b/gcc/ada/libgnat/s-parame__vxworks.ads @@ -53,9 +53,7 @@ package System.Parameters is -- Task And Stack Allocation Control -- --------------------------------------- - type Size_Type is range - -(2 ** (Integer'(Standard'Address_Size) - 1)) .. - +(2 ** (Integer'(Standard'Address_Size) - 1)) - 1; + type Size_Type is range -Memory_Size / 2 .. Memory_Size / 2 - 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 diff --git a/gcc/ada/libgnat/s-putima.adb b/gcc/ada/libgnat/s-putima.adb index 34d5a03..1d6e608 100644 --- a/gcc/ada/libgnat/s-putima.adb +++ b/gcc/ada/libgnat/s-putima.adb @@ -118,9 +118,8 @@ package body System.Put_Images is (S : in out Sink'Class; X : Long_Long_Long_Unsigned) renames LLL_Integer_Images.Put_Image; - type Signed_Address is range - -2**(Standard'Address_Size - 1) .. 2**(Standard'Address_Size - 1) - 1; - type Unsigned_Address is mod 2**Standard'Address_Size; + type Signed_Address is range -Memory_Size / 2 .. Memory_Size / 2 - 1; + type Unsigned_Address is mod Memory_Size; package Hex is new Generic_Integer_Images (Signed_Address, Unsigned_Address, Base => 16); diff --git a/gcc/ada/libgnat/s-regpat.adb b/gcc/ada/libgnat/s-regpat.adb index 256390f..80f7a8f 100644 --- a/gcc/ada/libgnat/s-regpat.adb +++ b/gcc/ada/libgnat/s-regpat.adb @@ -895,7 +895,7 @@ package body System.Regpat is Flags.SP_Start := Flags.SP_Start or else New_Flags.SP_Start; while Parse_Pos <= Parse_End - and then (E (Parse_Pos) = '|') + and then E (Parse_Pos) = '|' loop Parse_Pos := Parse_Pos + 1; Parse_Branch (New_Flags, False, Br); @@ -979,7 +979,7 @@ package body System.Regpat is C := Expression (Parse_Pos); Parse_Pos := Parse_Pos + 1; - case (C) is + case C is when '^' => IP := Emit_Node diff --git a/gcc/ada/libgnat/s-spcuop.ads b/gcc/ada/libgnat/s-spcuop.ads index daf550b6..642ded7 100644 --- a/gcc/ada/libgnat/s-spcuop.ads +++ b/gcc/ada/libgnat/s-spcuop.ads @@ -45,7 +45,7 @@ package System.SPARK.Cut_Operations with SPARK_Mode, Pure, - Annotate => (GNATprove, Always_Return) + Always_Terminates is function By (Consequence, Premise : Boolean) return Boolean with diff --git a/gcc/ada/libgnat/s-statxd.adb b/gcc/ada/libgnat/s-statxd.adb index dc45ee8..69412b8 100644 --- a/gcc/ada/libgnat/s-statxd.adb +++ b/gcc/ada/libgnat/s-statxd.adb @@ -295,8 +295,8 @@ package body System.Stream_Attributes.XDR is FP : Fat_Pointer; begin - FP.P1 := I_AS (Stream).P1; - FP.P2 := I_AS (Stream).P1; + FP.P1 := I_AS (Stream); + FP.P2 := I_AS (Stream); return FP; end I_AD; @@ -321,7 +321,7 @@ package body System.Stream_Attributes.XDR is U := U * BB + XDR_TM (S (N)); end loop; - return (P1 => To_XDR_SA (XDR_SA (U))); + return To_XDR_SA (XDR_SA (U)); end if; end I_AS; @@ -1181,7 +1181,7 @@ package body System.Stream_Attributes.XDR is procedure W_AS (Stream : not null access RST; Item : Thin_Pointer) is S : XDR_S_TM; - U : XDR_TM := XDR_TM (To_XDR_SA (Item.P1)); + U : XDR_TM := XDR_TM (To_XDR_SA (Item)); begin for N in reverse S'Range loop diff --git a/gcc/ada/libgnat/s-stchop.adb b/gcc/ada/libgnat/s-stchop.adb index 8d8cc60..e0efcef 100644 --- a/gcc/ada/libgnat/s-stchop.adb +++ b/gcc/ada/libgnat/s-stchop.adb @@ -234,11 +234,10 @@ package body System.Stack_Checking.Operations is -- it is essential to use our local copy of Stack. begin - if (Stack_Grows_Down and then - (not (Frame_Address <= My_Stack.Base))) + if (Stack_Grows_Down and then not (Frame_Address <= My_Stack.Base)) or else (not Stack_Grows_Down and then - (not (Frame_Address >= My_Stack.Base))) + not (Frame_Address >= My_Stack.Base)) then -- The returned Base is lower than the stored one, so assume that -- the original one wasn't right and use the current Frame_Address diff --git a/gcc/ada/libgnat/s-stoele.adb b/gcc/ada/libgnat/s-stoele.adb index e029f51..dfd1ba3 100644 --- a/gcc/ada/libgnat/s-stoele.adb +++ b/gcc/ada/libgnat/s-stoele.adb @@ -29,101 +29,8 @@ -- -- ------------------------------------------------------------------------------ -with Ada.Unchecked_Conversion; +-- This package does not require a body. We provide a dummy file containing a +-- No_Body pragma so that previous versions of the body (which did exist) will +-- not interfere. -package body System.Storage_Elements is - - pragma Suppress (All_Checks); - - -- Conversion to/from address - - -- Note qualification below of To_Address to avoid ambiguities systems - -- where Address is a visible integer type. - - function To_Address is - new Ada.Unchecked_Conversion (Storage_Offset, Address); - function To_Offset is - new Ada.Unchecked_Conversion (Address, Storage_Offset); - - -- Conversion to/from integers - - -- These functions must be place first because they are inlined_always - -- and are used and inlined in other subprograms defined in this unit. - - ---------------- - -- To_Address -- - ---------------- - - function To_Address (Value : Integer_Address) return Address is - begin - return Address (Value); - end To_Address; - - ---------------- - -- To_Integer -- - ---------------- - - function To_Integer (Value : Address) return Integer_Address is - begin - return Integer_Address (Value); - end To_Integer; - - -- Address arithmetic - - --------- - -- "+" -- - --------- - - function "+" (Left : Address; Right : Storage_Offset) return Address is - begin - return Storage_Elements.To_Address - (To_Integer (Left) + To_Integer (To_Address (Right))); - end "+"; - - function "+" (Left : Storage_Offset; Right : Address) return Address is - begin - return Storage_Elements.To_Address - (To_Integer (To_Address (Left)) + To_Integer (Right)); - end "+"; - - --------- - -- "-" -- - --------- - - function "-" (Left : Address; Right : Storage_Offset) return Address is - begin - return Storage_Elements.To_Address - (To_Integer (Left) - To_Integer (To_Address (Right))); - end "-"; - - function "-" (Left, Right : Address) return Storage_Offset is - begin - return To_Offset (Storage_Elements.To_Address - (To_Integer (Left) - To_Integer (Right))); - end "-"; - - ----------- - -- "mod" -- - ----------- - - function "mod" - (Left : Address; - Right : Storage_Offset) return Storage_Offset - is - begin - if Right > 0 then - return Storage_Offset - (To_Integer (Left) mod Integer_Address (Right)); - - -- The negative case makes no sense since it is a case of a mod where - -- the left argument is unsigned and the right argument is signed. In - -- accordance with the (spirit of the) permission of RM 13.7.1(16), - -- we raise CE, and also include the zero case here. Yes, the RM says - -- PE, but this really is so obviously more like a constraint error. - - else - raise Constraint_Error; - end if; - end "mod"; - -end System.Storage_Elements; +pragma No_Body; diff --git a/gcc/ada/libgnat/s-stoele.ads b/gcc/ada/libgnat/s-stoele.ads index 9fd31e7..d5d7042 100644 --- a/gcc/ada/libgnat/s-stoele.ads +++ b/gcc/ada/libgnat/s-stoele.ads @@ -37,26 +37,18 @@ -- extra declarations that can be introduced into System using Extend_System. -- It is a good idea to avoid use clauses for this package. -package System.Storage_Elements is +package System.Storage_Elements with + Always_Terminates +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 Annotate (GNATprove, Always_Return, Storage_Elements); + pragma No_Elaboration_Code_All; + -- Allow the use of that restriction in units that WITH this unit - -- We also add the pragma Pure_Function to the operations in this package, - -- because otherwise functions with parameters derived from Address are - -- treated as non-pure by the back-end (see exp_ch6.adb). This is because - -- in many cases such a parameter is used to hide read/out access to - -- objects, and it would be unsafe to treat such functions as pure. - - type Storage_Offset is range - -(2 ** (Integer'(Standard'Address_Size) - 1)) .. - +(2 ** (Integer'(Standard'Address_Size) - 1)) - Long_Long_Integer'(1); - -- Note: the reason for the Long_Long_Integer qualification here is to - -- avoid a bogus ambiguity when this unit is analyzed in an rtsfind - -- context. + type Storage_Offset is range -Memory_Size / 2 .. Memory_Size / 2 - 1; subtype Storage_Count is Storage_Offset range 0 .. Storage_Offset'Last; @@ -73,44 +65,26 @@ package System.Storage_Elements is -- Address arithmetic function "+" (Left : Address; Right : Storage_Offset) return Address; - pragma Convention (Intrinsic, "+"); - pragma Inline_Always ("+"); - pragma Pure_Function ("+"); - function "+" (Left : Storage_Offset; Right : Address) return Address; - pragma Convention (Intrinsic, "+"); - pragma Inline_Always ("+"); - pragma Pure_Function ("+"); + pragma Import (Intrinsic, "+"); function "-" (Left : Address; Right : Storage_Offset) return Address; - pragma Convention (Intrinsic, "-"); - pragma Inline_Always ("-"); - pragma Pure_Function ("-"); - function "-" (Left, Right : Address) return Storage_Offset; - pragma Convention (Intrinsic, "-"); - pragma Inline_Always ("-"); - pragma Pure_Function ("-"); + pragma Import (Intrinsic, "-"); function "mod" (Left : Address; - Right : Storage_Offset) return Storage_Offset; - pragma Convention (Intrinsic, "mod"); - pragma Inline_Always ("mod"); - pragma Pure_Function ("mod"); + Right : Storage_Offset) return Storage_Offset; + pragma Import (Intrinsic, "mod"); -- Conversion to/from integers type Integer_Address is mod Memory_Size; function To_Address (Value : Integer_Address) return Address; - pragma Convention (Intrinsic, To_Address); - pragma Inline_Always (To_Address); - pragma Pure_Function (To_Address); + pragma Import (Intrinsic, To_Address); function To_Integer (Value : Address) return Integer_Address; - pragma Convention (Intrinsic, To_Integer); - pragma Inline_Always (To_Integer); - pragma Pure_Function (To_Integer); + pragma Import (Intrinsic, To_Integer); end System.Storage_Elements; diff --git a/gcc/ada/libgnat/s-stratt.ads b/gcc/ada/libgnat/s-stratt.ads index e0ddc23..1a3fb60 100644 --- a/gcc/ada/libgnat/s-stratt.ads +++ b/gcc/ada/libgnat/s-stratt.ads @@ -67,9 +67,7 @@ package System.Stream_Attributes is -- (double address) form. The following types are used to hold access -- values using unchecked conversions. - type Thin_Pointer is record - P1 : System.Address; - end record; + subtype Thin_Pointer is System.Address; type Fat_Pointer is record P1 : System.Address; diff --git a/gcc/ada/libgnat/s-strcom.adb b/gcc/ada/libgnat/s-strcom.adb index 59e5698..a2354f3 100644 --- a/gcc/ada/libgnat/s-strcom.adb +++ b/gcc/ada/libgnat/s-strcom.adb @@ -70,7 +70,7 @@ package body System.String_Compare is begin -- If operands are non-aligned, or length is too short, go by bytes - if (((Left or Right) and 2#11#) /= 0) or else Compare_Len < 4 then + if ((Left or Right) and 2#11#) /= 0 or else Compare_Len < 4 then return Str_Compare_Bytes (Left, Right, Left_Len, Right_Len); end if; diff --git a/gcc/ada/libgnat/s-tsmona__linux.adb b/gcc/ada/libgnat/s-tsmona__linux.adb index 7e1b493..6b539f1 100644 --- a/gcc/ada/libgnat/s-tsmona__linux.adb +++ b/gcc/ada/libgnat/s-tsmona__linux.adb @@ -93,23 +93,30 @@ package body Module_Name is pragma Convention (C, link_map_acc); type link_map is record - l_addr : Address; + l_addr : aliased Address; -- Base address of the shared object - l_name : Address; + l_name : aliased Address; -- Null-terminated absolute file name - l_ld : Address; + l_ld : aliased Address; -- Dynamic section - l_next, l_prev : link_map_acc; + l_next, l_prev : aliased link_map_acc; -- Chain end record; pragma Convention (C, link_map); + type r_debug_state is (RT_CONSISTENT, RT_ADD, RT_DELETE); + pragma Convention (C, r_debug_state); + pragma Unreferenced (RT_CONSISTENT, RT_ADD, RT_DELETE); + type r_debug_type is record - r_version : Integer; - r_map : link_map_acc; + r_version : aliased int; + r_map : aliased link_map_acc; + r_brk : aliased Address; + r_state : aliased r_debug_state; + r_ldbase : aliased Address; end record; pragma Convention (C, r_debug_type); diff --git a/gcc/ada/libgnat/s-vaispe.ads b/gcc/ada/libgnat/s-vaispe.ads index 28efced..e74202d7 100644 --- a/gcc/ada/libgnat/s-vaispe.ads +++ b/gcc/ada/libgnat/s-vaispe.ads @@ -62,7 +62,7 @@ generic package System.Value_I_Spec with Ghost, SPARK_Mode, - Annotate => (GNATprove, Always_Return) + Always_Terminates is pragma Preelaborate; use all type Uns_Params.Uns_Option; diff --git a/gcc/ada/libgnat/s-valueu.adb b/gcc/ada/libgnat/s-valueu.adb index c6e26b0..9c77caa 100644 --- a/gcc/ada/libgnat/s-valueu.adb +++ b/gcc/ada/libgnat/s-valueu.adb @@ -29,6 +29,8 @@ -- -- ------------------------------------------------------------------------------ +with System.SPARK.Cut_Operations; use System.SPARK.Cut_Operations; + package body System.Value_U is -- Ghost code, loop invariants and assertions in this unit are meant for @@ -138,10 +140,7 @@ package body System.Value_U is Spec.Scan_Based_Number_Ghost (Str, Ptr.all, Last_Num_Init) with Ghost; Starts_As_Based : constant Boolean := - Last_Num_Init < Max - 1 - and then Str (Last_Num_Init + 1) in '#' | ':' - and then Str (Last_Num_Init + 2) in - '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' + Spec.Raw_Unsigned_Starts_As_Based_Ghost (Str, Last_Num_Init, Max) with Ghost; Last_Num_Based : constant Integer := (if Starts_As_Based @@ -149,9 +148,8 @@ package body System.Value_U is else Last_Num_Init) with Ghost; Is_Based : constant Boolean := - Starts_As_Based - and then Last_Num_Based < Max - and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1) + Spec.Raw_Unsigned_Is_Based_Ghost + (Str, Last_Num_Init, Last_Num_Based, Max) with Ghost; Based_Val : constant Spec.Uns_Option := (if Starts_As_Based and then not Init_Val.Overflow @@ -174,6 +172,7 @@ package body System.Value_U is P := Ptr.all; Spec.Lemma_Scan_Based_Number_Ghost_Step (Str, P, Last_Num_Init); Uval := Character'Pos (Str (P)) - Character'Pos ('0'); + pragma Assert (Str (P) in '0' .. '9'); P := P + 1; -- Scan out digits of what is either the number or the base. @@ -215,19 +214,24 @@ package body System.Value_U is -- Accumulate result, checking for overflow else + pragma Assert + (By + (Str (P) in '0' .. '9', + By + (Character'Pos (Str (P)) >= Character'Pos ('0'), + Uns '(Character'Pos (Str (P))) >= + Character'Pos ('0')))); Spec.Lemma_Scan_Based_Number_Ghost_Step (Str, P, Last_Num_Init, Acc => Uval); Spec.Lemma_Scan_Based_Number_Ghost_Overflow (Str, P, Last_Num_Init, Acc => Uval); if Uval <= Umax then - pragma Assert - (Spec.Hexa_To_Unsigned_Ghost (Str (P)) = Digit); Uval := 10 * Uval + Digit; pragma Assert (if not Overflow then Init_Val = Spec.Scan_Based_Number_Ghost - (Str, P + 1, Last_Num_Init, Acc => Uval)); + (Str, P + 1, Last_Num_Init, Acc => Uval)); elsif Uval > Umax10 then Overflow := True; @@ -241,7 +245,8 @@ package body System.Value_U is pragma Assert (if not Overflow then Init_Val = Spec.Scan_Based_Number_Ghost - (Str, P + 1, Last_Num_Init, Acc => Uval)); + (Str, P + 1, Last_Num_Init, Acc => Uval)); + end if; P := P + 1; @@ -252,7 +257,9 @@ package body System.Value_U is end; pragma Assert_And_Cut - (P = Last_Num_Init + 1 + (By + (P = Last_Num_Init + 1, + P > Max or else Str (P) not in '_' | '0' .. '9') and then Overflow = Init_Val.Overflow and then (if not Overflow then Init_Val.Value = Uval)); @@ -313,13 +320,24 @@ package body System.Value_U is -- already stored in Ptr.all. else + pragma Assert + (By + (Spec.Only_Hexa_Ghost (Str, P, Last_Num_Based), + P > Last_Num_Init + 1 + and Spec.Only_Hexa_Ghost + (Str, Last_Num_Init + 2, Last_Num_Based))); Spec.Lemma_Scan_Based_Number_Ghost_Base (Str, P, Last_Num_Based, Base, Uval); Uval := Base; Base := 10; pragma Assert (Ptr.all = Last_Num_Init + 1); pragma Assert - (if Starts_As_Based then P = Last_Num_Based + 1); + (if Starts_As_Based + then By + (P = Last_Num_Based + 1, + P <= Last_Num_Based + 1 + and Str (P) not in + '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_')); pragma Assert (not Is_Based); pragma Assert (if not Overflow then Uval = Init_Val.Value); exit; @@ -394,11 +412,15 @@ package body System.Value_U is Ptr.all := P + 1; pragma Assert (P = Last_Num_Based + 1); pragma Assert (Ptr.all = Last_Num_Based + 2); - pragma Assert (Starts_As_Based); - pragma Assert (Last_Num_Based < Max); - pragma Assert (Str (Last_Num_Based + 1) = Base_Char); - pragma Assert (Base_Char = Str (Last_Num_Init + 1)); - pragma Assert (Is_Based); + pragma Assert + (By + (Is_Based, + So + (Starts_As_Based, + So + (Last_Num_Based < Max, + Str (Last_Num_Based + 1) = Base_Char + and Base_Char = Str (Last_Num_Init + 1))))); Spec.Lemma_Scan_Based_Number_Ghost_Base (Str, P, Last_Num_Based, Base, Uval); exit; @@ -414,41 +436,40 @@ package body System.Value_U is (if not Overflow then Based_Val = Spec.Scan_Based_Number_Ghost (Str, P, Last_Num_Based, Base, Uval)); - pragma Assert (Str (P) /= '_'); - pragma Assert (Str (P) /= Base_Char); + pragma Assert (Str (P) not in '_' | Base_Char); end if; Lemma_Digit_Not_Last (Str, P, Last_Num_Init + 2, Max); - pragma Assert (Str (P) /= '_'); - pragma Assert (Str (P) /= Base_Char); + pragma Assert (Str (P) not in '_' | Base_Char); end loop; end; pragma Assert (if Starts_As_Based then P = Last_Num_Based + 1 else P = Last_Num_Init + 2); pragma Assert - (Last_Num_Init < Max - 1 - and then Str (Last_Num_Init + 1) in '#' | ':'); - pragma Assert - (Overflow = - (Init_Val.Overflow - or else Init_Val.Value not in 2 .. 16 - or else (Starts_As_Based and then Based_Val.Overflow))); - pragma Assert - (Overflow /= Spec.Scan_Split_No_Overflow_Ghost (Str, Ptr_Old, Max)); + (By + (Overflow /= Spec.Scan_Split_No_Overflow_Ghost + (Str, Ptr_Old, Max), + So + (Last_Num_Init < Max - 1 + and then Str (Last_Num_Init + 1) in '#' | ':', + Overflow = + (Init_Val.Overflow + or else Init_Val.Value not in 2 .. 16 + or else (Starts_As_Based and Based_Val.Overflow))))); end if; pragma Assert_And_Cut (Overflow /= Spec.Scan_Split_No_Overflow_Ghost (Str, Ptr_Old, Max) - and then - (if not Overflow then - (if Is_Based then Uval = Based_Val.Value - else Uval = Init_Val.Value)) and then Ptr.all = First_Exp and then Base in 2 .. 16 and then (if not Overflow then - (if Is_Based then Base = Init_Val.Value else Base = 10))); + (if Is_Based then Base = Init_Val.Value else Base = 10)) + and then + (if not Overflow then + (if Is_Based then Uval = Based_Val.Value + else Uval = Init_Val.Value))); -- Come here with scanned unsigned value in Uval. The only remaining -- required step is to deal with exponent if one is present. @@ -456,7 +477,14 @@ package body System.Value_U is Scan_Exponent (Str, Ptr, Max, Expon); pragma Assert - (Ptr.all = Spec.Raw_Unsigned_Last_Ghost (Str, Ptr_Old, Max)); + (By + (Ptr.all = Spec.Raw_Unsigned_Last_Ghost (Str, Ptr_Old, Max), + Ptr.all = + (if not Starts_As_Exponent_Format_Ghost (Str (First_Exp .. Max)) + then First_Exp + elsif Str (First_Exp + 1) in '-' | '+' then + Last_Number_Ghost (Str (First_Exp + 2 .. Max)) + 1 + else Last_Number_Ghost (Str (First_Exp + 1 .. Max)) + 1))); pragma Assert (if not Overflow then Spec.Scan_Split_Value_Ghost (Str, Ptr_Old, Max) = diff --git a/gcc/ada/libgnat/s-valuti.adb b/gcc/ada/libgnat/s-valuti.adb index ec6fdb0..ee37c1a 100644 --- a/gcc/ada/libgnat/s-valuti.adb +++ b/gcc/ada/libgnat/s-valuti.adb @@ -123,6 +123,7 @@ is while F < L and then S (F) = ' ' loop pragma Loop_Invariant (F in S'First .. L - 1); pragma Loop_Invariant (for all J in S'First .. F => S (J) = ' '); + pragma Loop_Variant (Increases => F); F := F + 1; end loop; @@ -139,6 +140,7 @@ is while S (L) = ' ' loop pragma Loop_Invariant (L in F + 1 .. S'Last); pragma Loop_Invariant (for all J in L .. S'Last => S (J) = ' '); + pragma Loop_Variant (Decreases => L); L := L - 1; end loop; diff --git a/gcc/ada/libgnat/s-valuti.ads b/gcc/ada/libgnat/s-valuti.ads index 1faa647..22d0612 100644 --- a/gcc/ada/libgnat/s-valuti.ads +++ b/gcc/ada/libgnat/s-valuti.ads @@ -51,7 +51,8 @@ is procedure Bad_Value (S : String) with - Depends => (null => S); + Depends => (null => S), + Exceptional_Cases => (others => Standard.False); pragma No_Return (Bad_Value); -- Raises constraint error with message: bad input for 'Value: "xxx" diff --git a/gcc/ada/libgnat/s-vauspe.ads b/gcc/ada/libgnat/s-vauspe.ads index 25a095b..bdd97b5 100644 --- a/gcc/ada/libgnat/s-vauspe.ads +++ b/gcc/ada/libgnat/s-vauspe.ads @@ -53,7 +53,7 @@ generic package System.Value_U_Spec with Ghost, SPARK_Mode, - Annotate => (GNATprove, Always_Return) + Always_Terminates is pragma Preelaborate; @@ -279,24 +279,50 @@ is Exponent_Unsigned_Ghost (Value * Base, Exp - 1, Base)); -- Normal case: exponentiation without overflows + function Raw_Unsigned_Starts_As_Based_Ghost + (Str : String; + Last_Num_Init, To : Integer) + return Boolean + is + (Last_Num_Init < To - 1 + and then Str (Last_Num_Init + 1) in '#' | ':' + and then Str (Last_Num_Init + 2) in + '0' .. '9' | 'a' .. 'f' | 'A' .. 'F') + with Ghost, + Pre => Last_Num_Init in Str'Range + and then To in Str'Range; + -- Return True if Str starts as a based number + + function Raw_Unsigned_Is_Based_Ghost + (Str : String; + Last_Num_Init : Integer; + Last_Num_Based : Integer; + To : Integer) + return Boolean + is + (Raw_Unsigned_Starts_As_Based_Ghost (Str, Last_Num_Init, To) + and then Last_Num_Based < To + and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1)) + with Ghost, + Pre => Last_Num_Init in Str'Range + and then Last_Num_Based in Last_Num_Init .. Str'Last + and then To in Str'Range; + -- Return True if Str is a based number + function Is_Raw_Unsigned_Format_Ghost (Str : String) return Boolean is (Is_Natural_Format_Ghost (Str) and then (declare Last_Num_Init : constant Integer := Last_Number_Ghost (Str); Starts_As_Based : constant Boolean := - Last_Num_Init < Str'Last - 1 - and then Str (Last_Num_Init + 1) in '#' | ':' - and then Str (Last_Num_Init + 2) in - '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'; + Raw_Unsigned_Starts_As_Based_Ghost (Str, Last_Num_Init, Str'Last); Last_Num_Based : constant Integer := (if Starts_As_Based then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. Str'Last)) else Last_Num_Init); Is_Based : constant Boolean := - Starts_As_Based - and then Last_Num_Based < Str'Last - and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1); + Raw_Unsigned_Is_Based_Ghost + (Str, Last_Num_Init, Last_Num_Based, Str'Last); First_Exp : constant Integer := (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1); begin @@ -330,10 +356,7 @@ is Init_Val : constant Uns_Option := Scan_Based_Number_Ghost (Str, From, Last_Num_Init); Starts_As_Based : constant Boolean := - Last_Num_Init < To - 1 - and then Str (Last_Num_Init + 1) in '#' | ':' - and then Str (Last_Num_Init + 2) in - '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'; + Raw_Unsigned_Starts_As_Based_Ghost (Str, Last_Num_Init, To); Last_Num_Based : constant Integer := (if Starts_As_Based then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To)) @@ -378,18 +401,13 @@ is Init_Val : constant Uns_Option := Scan_Based_Number_Ghost (Str, From, Last_Num_Init); Starts_As_Based : constant Boolean := - Last_Num_Init < To - 1 - and then Str (Last_Num_Init + 1) in '#' | ':' - and then Str (Last_Num_Init + 2) in - '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'; + Raw_Unsigned_Starts_As_Based_Ghost (Str, Last_Num_Init, To); Last_Num_Based : constant Integer := (if Starts_As_Based then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To)) else Last_Num_Init); Is_Based : constant Boolean := - Starts_As_Based - and then Last_Num_Based < To - and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1); + Raw_Unsigned_Is_Based_Ghost (Str, Last_Num_Init, Last_Num_Based, To); Based_Val : constant Uns_Option := (if Starts_As_Based and then not Init_Val.Overflow then Scan_Based_Number_Ghost @@ -468,18 +486,13 @@ is Last_Num_Init : constant Integer := Last_Number_Ghost (Str (From .. To)); Starts_As_Based : constant Boolean := - Last_Num_Init < To - 1 - and then Str (Last_Num_Init + 1) in '#' | ':' - and then Str (Last_Num_Init + 2) in - '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'; + Raw_Unsigned_Starts_As_Based_Ghost (Str, Last_Num_Init, To); Last_Num_Based : constant Integer := (if Starts_As_Based then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To)) else Last_Num_Init); Is_Based : constant Boolean := - Starts_As_Based - and then Last_Num_Based < To - and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1); + Raw_Unsigned_Is_Based_Ghost (Str, Last_Num_Init, Last_Num_Based, To); First_Exp : constant Integer := (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1); begin @@ -492,7 +505,8 @@ is Pre => Str'Last /= Positive'Last and then From in Str'Range and then To in From .. Str'Last - and then Str (From) in '0' .. '9'; + and then Str (From) in '0' .. '9', + Post => Raw_Unsigned_Last_Ghost'Result >= From; -- Ghost function that returns the position of the cursor once an unsigned -- number has been seen. diff --git a/gcc/ada/libgnat/s-widthi.adb b/gcc/ada/libgnat/s-widthi.adb index bdd1bfb..7f04e22 100644 --- a/gcc/ada/libgnat/s-widthi.adb +++ b/gcc/ada/libgnat/s-widthi.adb @@ -166,9 +166,9 @@ begin 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; + F : constant Big_Positive := Big_10 ** (W - 2) with Ghost; + Q : constant Big_Natural := Big (T_Init) / F with Ghost; + R : constant Big_Natural := Big (T_Init) rem F with Ghost; begin pragma Assert (Q < Big_10); pragma Assert (Big (T_Init) = Q * F + R); diff --git a/gcc/ada/libgnat/system-aix.ads b/gcc/ada/libgnat/system-aix.ads index 18ed063..1485df4 100644 --- a/gcc/ada/libgnat/system-aix.ads +++ b/gcc/ada/libgnat/system-aix.ads @@ -116,6 +116,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-darwin-arm.ads b/gcc/ada/libgnat/system-darwin-arm.ads index 4e4603b..a57bf0b 100644 --- a/gcc/ada/libgnat/system-darwin-arm.ads +++ b/gcc/ada/libgnat/system-darwin-arm.ads @@ -132,6 +132,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-darwin-ppc.ads b/gcc/ada/libgnat/system-darwin-ppc.ads index 80c28c5..b6e73fd 100644 --- a/gcc/ada/libgnat/system-darwin-ppc.ads +++ b/gcc/ada/libgnat/system-darwin-ppc.ads @@ -132,6 +132,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-darwin-x86.ads b/gcc/ada/libgnat/system-darwin-x86.ads index dc52576..994b22f 100644 --- a/gcc/ada/libgnat/system-darwin-x86.ads +++ b/gcc/ada/libgnat/system-darwin-x86.ads @@ -132,6 +132,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-djgpp.ads b/gcc/ada/libgnat/system-djgpp.ads index 2addbfe..459475e 100644 --- a/gcc/ada/libgnat/system-djgpp.ads +++ b/gcc/ada/libgnat/system-djgpp.ads @@ -106,6 +106,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-dragonfly-x86_64.ads b/gcc/ada/libgnat/system-dragonfly-x86_64.ads index 0e8e0ee5..6b16156 100644 --- a/gcc/ada/libgnat/system-dragonfly-x86_64.ads +++ b/gcc/ada/libgnat/system-dragonfly-x86_64.ads @@ -106,6 +106,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-freebsd.ads b/gcc/ada/libgnat/system-freebsd.ads index 23bb9a7..32c1cc4 100644 --- a/gcc/ada/libgnat/system-freebsd.ads +++ b/gcc/ada/libgnat/system-freebsd.ads @@ -107,6 +107,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-hpux-ia64.ads b/gcc/ada/libgnat/system-hpux-ia64.ads index 991ff9e..8eb4a8f 100644 --- a/gcc/ada/libgnat/system-hpux-ia64.ads +++ b/gcc/ada/libgnat/system-hpux-ia64.ads @@ -106,6 +106,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-hpux.ads b/gcc/ada/libgnat/system-hpux.ads index 30e0293..4c5eb3e 100644 --- a/gcc/ada/libgnat/system-hpux.ads +++ b/gcc/ada/libgnat/system-hpux.ads @@ -106,6 +106,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-linux-alpha.ads b/gcc/ada/libgnat/system-linux-alpha.ads index 021a9aa..86fcea3 100644 --- a/gcc/ada/libgnat/system-linux-alpha.ads +++ b/gcc/ada/libgnat/system-linux-alpha.ads @@ -106,6 +106,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-linux-arm.ads b/gcc/ada/libgnat/system-linux-arm.ads index 0c94244..724086c 100644 --- a/gcc/ada/libgnat/system-linux-arm.ads +++ b/gcc/ada/libgnat/system-linux-arm.ads @@ -115,6 +115,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-linux-hppa.ads b/gcc/ada/libgnat/system-linux-hppa.ads index 41a8d3f..148b6f0 100644 --- a/gcc/ada/libgnat/system-linux-hppa.ads +++ b/gcc/ada/libgnat/system-linux-hppa.ads @@ -106,6 +106,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-linux-ia64.ads b/gcc/ada/libgnat/system-linux-ia64.ads index a788eb2..d332820 100644 --- a/gcc/ada/libgnat/system-linux-ia64.ads +++ b/gcc/ada/libgnat/system-linux-ia64.ads @@ -114,6 +114,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-linux-m68k.ads b/gcc/ada/libgnat/system-linux-m68k.ads index 669428b..9db322b 100644 --- a/gcc/ada/libgnat/system-linux-m68k.ads +++ b/gcc/ada/libgnat/system-linux-m68k.ads @@ -116,6 +116,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-linux-mips.ads b/gcc/ada/libgnat/system-linux-mips.ads index a40a0d2..929e54b 100644 --- a/gcc/ada/libgnat/system-linux-mips.ads +++ b/gcc/ada/libgnat/system-linux-mips.ads @@ -107,6 +107,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-linux-ppc.ads b/gcc/ada/libgnat/system-linux-ppc.ads index a24d616..1358bf9 100644 --- a/gcc/ada/libgnat/system-linux-ppc.ads +++ b/gcc/ada/libgnat/system-linux-ppc.ads @@ -115,6 +115,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- @@ -142,6 +144,7 @@ private Stack_Check_Probes : constant Boolean := True; Stack_Check_Limits : constant Boolean := False; 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; diff --git a/gcc/ada/libgnat/system-linux-riscv.ads b/gcc/ada/libgnat/system-linux-riscv.ads index 8f8f6e6..420a502 100644 --- a/gcc/ada/libgnat/system-linux-riscv.ads +++ b/gcc/ada/libgnat/system-linux-riscv.ads @@ -106,6 +106,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-linux-s390.ads b/gcc/ada/libgnat/system-linux-s390.ads index dee2424..f53c43f 100644 --- a/gcc/ada/libgnat/system-linux-s390.ads +++ b/gcc/ada/libgnat/system-linux-s390.ads @@ -106,6 +106,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-linux-sh4.ads b/gcc/ada/libgnat/system-linux-sh4.ads index 52c67b6..4970b28 100644 --- a/gcc/ada/libgnat/system-linux-sh4.ads +++ b/gcc/ada/libgnat/system-linux-sh4.ads @@ -114,6 +114,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-linux-sparc.ads b/gcc/ada/libgnat/system-linux-sparc.ads index 4b4978b..a319664 100644 --- a/gcc/ada/libgnat/system-linux-sparc.ads +++ b/gcc/ada/libgnat/system-linux-sparc.ads @@ -106,6 +106,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-linux-x86.ads b/gcc/ada/libgnat/system-linux-x86.ads index ec17297..85538d6 100644 --- a/gcc/ada/libgnat/system-linux-x86.ads +++ b/gcc/ada/libgnat/system-linux-x86.ads @@ -114,6 +114,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-lynxos178-ppc.ads b/gcc/ada/libgnat/system-lynxos178-ppc.ads index 75f17b2..a0ef4118 100644 --- a/gcc/ada/libgnat/system-lynxos178-ppc.ads +++ b/gcc/ada/libgnat/system-lynxos178-ppc.ads @@ -121,6 +121,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-lynxos178-x86.ads b/gcc/ada/libgnat/system-lynxos178-x86.ads index 0f4caea..8c8a61e 100644 --- a/gcc/ada/libgnat/system-lynxos178-x86.ads +++ b/gcc/ada/libgnat/system-lynxos178-x86.ads @@ -121,6 +121,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-mingw.ads b/gcc/ada/libgnat/system-mingw.ads index af1cb20..4b5a7ce 100644 --- a/gcc/ada/libgnat/system-mingw.ads +++ b/gcc/ada/libgnat/system-mingw.ads @@ -106,6 +106,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-qnx-arm.ads b/gcc/ada/libgnat/system-qnx-arm.ads index e834399..1dd1a22 100644 --- a/gcc/ada/libgnat/system-qnx-arm.ads +++ b/gcc/ada/libgnat/system-qnx-arm.ads @@ -95,26 +95,26 @@ package System is -- Priority-related Declarations (RM D.1) - -- System priority is Ada priority + 1, so lies in the range 1 .. 63. - -- -- If the scheduling policy is SCHED_FIFO or SCHED_RR the runtime makes use -- of the entire range provided by the system. -- -- If the scheduling policy is SCHED_OTHER the only valid system priority -- is 1 and other values are simply ignored. - Max_Priority : constant Positive := 61; - Max_Interrupt_Priority : constant Positive := 62; + Max_Priority : constant Positive := 62; + Max_Interrupt_Priority : constant Positive := 63; - subtype Any_Priority is Integer range 0 .. 62; - subtype Priority is Any_Priority range 0 .. 61; - subtype Interrupt_Priority is Any_Priority range 62 .. 62; + subtype Any_Priority is Integer range 1 .. 63; + subtype Priority is Any_Priority range 1 .. 62; + subtype Interrupt_Priority is Any_Priority range 63 .. 63; - Default_Priority : constant Priority := 30; + Default_Priority : constant Priority := 10; private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-rtems.ads b/gcc/ada/libgnat/system-rtems.ads index 6518ada..2dc2d81 100644 --- a/gcc/ada/libgnat/system-rtems.ads +++ b/gcc/ada/libgnat/system-rtems.ads @@ -123,6 +123,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-solaris-sparc.ads b/gcc/ada/libgnat/system-solaris-sparc.ads index e667cd5..7bd8460 100644 --- a/gcc/ada/libgnat/system-solaris-sparc.ads +++ b/gcc/ada/libgnat/system-solaris-sparc.ads @@ -106,6 +106,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-solaris-x86.ads b/gcc/ada/libgnat/system-solaris-x86.ads index b1a2733..6077668 100644 --- a/gcc/ada/libgnat/system-solaris-x86.ads +++ b/gcc/ada/libgnat/system-solaris-x86.ads @@ -106,6 +106,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-vxworks-ppc-kernel.ads b/gcc/ada/libgnat/system-vxworks-ppc-kernel.ads index e57b195..f12dc6e 100644 --- a/gcc/ada/libgnat/system-vxworks-ppc-kernel.ads +++ b/gcc/ada/libgnat/system-vxworks-ppc-kernel.ads @@ -119,6 +119,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-vxworks-ppc-rtp-smp.ads b/gcc/ada/libgnat/system-vxworks-ppc-rtp-smp.ads index ff7c0e6..d8c498f 100644 --- a/gcc/ada/libgnat/system-vxworks-ppc-rtp-smp.ads +++ b/gcc/ada/libgnat/system-vxworks-ppc-rtp-smp.ads @@ -125,6 +125,8 @@ private -- Setup proper set of -L's for this configuration type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-vxworks-ppc-rtp.ads b/gcc/ada/libgnat/system-vxworks-ppc-rtp.ads index deb7f5f..3a3d336 100644 --- a/gcc/ada/libgnat/system-vxworks-ppc-rtp.ads +++ b/gcc/ada/libgnat/system-vxworks-ppc-rtp.ads @@ -124,6 +124,8 @@ private -- Setup proper set of -L's for this configuration type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-vxworks7-aarch64-rtp-smp.ads b/gcc/ada/libgnat/system-vxworks7-aarch64-rtp-smp.ads index 3df8b7b..0a7886b 100644 --- a/gcc/ada/libgnat/system-vxworks7-aarch64-rtp-smp.ads +++ b/gcc/ada/libgnat/system-vxworks7-aarch64-rtp-smp.ads @@ -124,6 +124,8 @@ private -- Define the symbol wrs_rtp_base type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-vxworks7-aarch64.ads b/gcc/ada/libgnat/system-vxworks7-aarch64.ads index 103e9497..811fac1 100644 --- a/gcc/ada/libgnat/system-vxworks7-aarch64.ads +++ b/gcc/ada/libgnat/system-vxworks7-aarch64.ads @@ -121,6 +121,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-vxworks7-arm-rtp-smp.ads b/gcc/ada/libgnat/system-vxworks7-arm-rtp-smp.ads index fae23b1..abdc200 100644 --- a/gcc/ada/libgnat/system-vxworks7-arm-rtp-smp.ads +++ b/gcc/ada/libgnat/system-vxworks7-arm-rtp-smp.ads @@ -121,6 +121,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-vxworks7-arm.ads b/gcc/ada/libgnat/system-vxworks7-arm.ads index 2fa7ed8..0e5e3e6 100644 --- a/gcc/ada/libgnat/system-vxworks7-arm.ads +++ b/gcc/ada/libgnat/system-vxworks7-arm.ads @@ -119,6 +119,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-vxworks7-ppc-kernel.ads b/gcc/ada/libgnat/system-vxworks7-ppc-kernel.ads index ed250e5..bbf6d98 100644 --- a/gcc/ada/libgnat/system-vxworks7-ppc-kernel.ads +++ b/gcc/ada/libgnat/system-vxworks7-ppc-kernel.ads @@ -119,6 +119,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- @@ -146,7 +148,7 @@ private Stack_Check_Probes : constant Boolean := True; Stack_Check_Limits : constant Boolean := False; Support_Aggregates : constant Boolean := True; - Support_Atomic_Primitives : constant Boolean := False; + Support_Atomic_Primitives : constant Boolean := True; Support_Composite_Assign : constant Boolean := True; Support_Composite_Compare : constant Boolean := True; Support_Long_Shifts : constant Boolean := True; diff --git a/gcc/ada/libgnat/system-vxworks7-ppc-rtp-smp.ads b/gcc/ada/libgnat/system-vxworks7-ppc-rtp-smp.ads index 503c326..de1e10d 100644 --- a/gcc/ada/libgnat/system-vxworks7-ppc-rtp-smp.ads +++ b/gcc/ada/libgnat/system-vxworks7-ppc-rtp-smp.ads @@ -124,6 +124,8 @@ private -- Define the symbol wrs_rtp_base type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- @@ -151,7 +153,7 @@ private Stack_Check_Probes : constant Boolean := True; Stack_Check_Limits : constant Boolean := False; Support_Aggregates : constant Boolean := True; - Support_Atomic_Primitives : constant Boolean := False; + Support_Atomic_Primitives : constant Boolean := True; Support_Composite_Assign : constant Boolean := True; Support_Composite_Compare : constant Boolean := True; Support_Long_Shifts : constant Boolean := True; diff --git a/gcc/ada/libgnat/system-vxworks7-ppc64-kernel.ads b/gcc/ada/libgnat/system-vxworks7-ppc64-kernel.ads index 1d5d592..f4f1af5 100644 --- a/gcc/ada/libgnat/system-vxworks7-ppc64-kernel.ads +++ b/gcc/ada/libgnat/system-vxworks7-ppc64-kernel.ads @@ -121,6 +121,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-vxworks7-ppc64-rtp-smp.ads b/gcc/ada/libgnat/system-vxworks7-ppc64-rtp-smp.ads index b55f289..4868891 100644 --- a/gcc/ada/libgnat/system-vxworks7-ppc64-rtp-smp.ads +++ b/gcc/ada/libgnat/system-vxworks7-ppc64-rtp-smp.ads @@ -124,6 +124,8 @@ private -- Define the symbol wrs_rtp_base type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-vxworks7-x86-kernel.ads b/gcc/ada/libgnat/system-vxworks7-x86-kernel.ads index 4710098..e60e122 100644 --- a/gcc/ada/libgnat/system-vxworks7-x86-kernel.ads +++ b/gcc/ada/libgnat/system-vxworks7-x86-kernel.ads @@ -119,6 +119,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-vxworks7-x86-rtp-smp.ads b/gcc/ada/libgnat/system-vxworks7-x86-rtp-smp.ads index 867e39f..b8a25a3 100644 --- a/gcc/ada/libgnat/system-vxworks7-x86-rtp-smp.ads +++ b/gcc/ada/libgnat/system-vxworks7-x86-rtp-smp.ads @@ -122,6 +122,8 @@ private -- Define the symbol wrs_rtp_base type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-vxworks7-x86_64-kernel.ads b/gcc/ada/libgnat/system-vxworks7-x86_64-kernel.ads index dc00937..273529f 100644 --- a/gcc/ada/libgnat/system-vxworks7-x86_64-kernel.ads +++ b/gcc/ada/libgnat/system-vxworks7-x86_64-kernel.ads @@ -119,6 +119,8 @@ package System is private type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- diff --git a/gcc/ada/libgnat/system-vxworks7-x86_64-rtp-smp.ads b/gcc/ada/libgnat/system-vxworks7-x86_64-rtp-smp.ads index 501ee72..a2ea30a 100644 --- a/gcc/ada/libgnat/system-vxworks7-x86_64-rtp-smp.ads +++ b/gcc/ada/libgnat/system-vxworks7-x86_64-rtp-smp.ads @@ -122,6 +122,8 @@ private -- Define the symbol wrs_rtp_base type Address is mod Memory_Size; + for Address'Size use Standard'Address_Size; + Null_Address : constant Address := 0; -------------------------------------- |