From: Joffrey Huguet <[email protected]>
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.
Tested on x86_64-pc-linux-gnu, committed on master.
---
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 e4a814dd1d0..3aa389aea7f 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 f6e2cf2a6fb..cb1e8fe47e5 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 --
--
2.53.0
