https://gcc.gnu.org/g:eabec6df0cb4c9f2ce94e06344a922d264305435
commit r17-1967-geabec6df0cb4c9f2ce94e06344a922d264305435 Author: Joffrey Huguet <[email protected]> Date: Mon Jun 15 17:44:35 2026 +0200 ada: Add global contracts to Ada.Command_Line subprograms This patch adds an abstract state defined in Ada.Command_Line and global contracts to subprograms defined in this unit. gcc/ada/ChangeLog: * libgnat/a-comlin.ads (Argument_Count): Add global contract. (Argument): Likewise. (Command_Name): Likewise. (Set_Exit_Status): Likewise. * libgnat/a-comlin.adb: Refine abstract state. Diff: --- gcc/ada/libgnat/a-comlin.adb | 4 +++- gcc/ada/libgnat/a-comlin.ads | 17 ++++++++++++----- 2 files changed, 15 insertions(+), 6 deletions(-) diff --git a/gcc/ada/libgnat/a-comlin.adb b/gcc/ada/libgnat/a-comlin.adb index e4a814dd1d07..3aa389aea7f0 100644 --- a/gcc/ada/libgnat/a-comlin.adb +++ b/gcc/ada/libgnat/a-comlin.adb @@ -31,7 +31,9 @@ with System; use System; -package body Ada.Command_Line is +package body Ada.Command_Line with + Refined_State => (Program_Exit_Status => null) +is function Arg_Count return Natural; pragma Import (C, Arg_Count, "__gnat_arg_count"); diff --git a/gcc/ada/libgnat/a-comlin.ads b/gcc/ada/libgnat/a-comlin.ads index f6e2cf2a6fbd..cb1e8fe47e5c 100644 --- a/gcc/ada/libgnat/a-comlin.ads +++ b/gcc/ada/libgnat/a-comlin.ads @@ -37,10 +37,14 @@ -- command line arguments and to set the exit status of the program as defined -- by ARM A.15. -package Ada.Command_Line is +package Ada.Command_Line with + Abstract_State => (Program_Exit_Status), + Initializes => (Program_Exit_Status) +is pragma Preelaborate; - function Argument_Count return Natural; + function Argument_Count return Natural with + Global => null; -- If the external execution environment supports passing arguments to a -- program, then Argument_Count returns the number of arguments passed to -- the program invoking the function. Otherwise it return 0. @@ -54,7 +58,8 @@ package Ada.Command_Line is -- SPARK does not yet support raise expressions. function Argument (Number : Positive) return String with - Pre => Number <= Argument_Count; + Pre => Number <= Argument_Count, + Global => null; -- If the external execution environment supports passing arguments to -- a program, then Argument returns an implementation-defined value -- corresponding to the argument at relative position Number. If Number @@ -63,7 +68,8 @@ package Ada.Command_Line is -- -- in GNAT: Corresponds to argv [n] (for n > 0) in C. - function Command_Name return String; + function Command_Name return String with + Global => null; -- If the external execution environment supports passing arguments to -- a program, then Command_Name returns an implementation-defined value -- corresponding to the name of the command invoking the program. @@ -76,7 +82,8 @@ package Ada.Command_Line is Success : constant Exit_Status; Failure : constant Exit_Status; - procedure Set_Exit_Status (Code : Exit_Status); + procedure Set_Exit_Status (Code : Exit_Status) with + Global => (Output => Program_Exit_Status); ------------------------------------ -- Note on Interface Requirements --
