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 --git a/gcc/ada/libgnat/a-comlin.adb b/gcc/ada/libgnat/a-comlin.adb
index e4a814dd1d07dc02c267af68a554abbf2e06e8d3..3aa389aea7f03c6e6f2062c3121de29226492e3a 100644 (file)
--- 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 f6e2cf2a6fbd7875a22dbf2acd15bf4bf488f825..cb1e8fe47e5cf4de72ff2ff7676fdb8d5dc4f2e4 100644 (file)
--- 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 --