[gcc r13-4361] ada: Annotate GNAT.Source_Info with an abstract state

[gcc r13-4361] ada: Annotate GNAT.Source_Info with an abstract state

[Marc Poulhi?s]

https://gcc.gnu.org/g:80ad275cf1e6f308d3bbafc34635eb56851d6862

commit r13-4361-g80ad275cf1e6f308d3bbafc34635eb56851d6862
Author: Claire Dross <dross@adacore.com>
Date:   Fri Nov 25 16:28:47 2022 +0100

    ada: Annotate GNAT.Source_Info with an abstract state
    
    So it can be used safely from SPARK code. The abstract state represents
    the source code information that is accessed by the functions defined
    in Source_Info. It is volatile as it is updated asyncronously when
    moving in the code.
    
    gcc/ada/
    
            * libgnat/g-souinf.ads (Source_Code_Information): Add a new
            volatile abstract state and add it in the global contract of all
            functions defined in Source_Info.

Diff:
---
 gcc/ada/libgnat/g-souinf.ads | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

diff --git a/gcc/ada/libgnat/g-souinf.ads b/gcc/ada/libgnat/g-souinf.ads
index 700f5180c82..6b72a6497f1 100644
--- a/gcc/ada/libgnat/g-souinf.ads
+++ b/gcc/ada/libgnat/g-souinf.ads
@@ -36,7 +36,13 @@
 --  and logging purposes. For example, an exception handler can print out
 --  the name of the source file in which the exception is handled.
 
-package GNAT.Source_Info is
+package GNAT.Source_Info with
+   SPARK_Mode,
+   Abstract_State =>
+     (Source_Code_Information with
+         External => (Async_Writers, Async_Readers)),
+   Annotate => (GNATprove, Always_Return)
+is
    pragma Preelaborate;
    --  Note that this unit is Preelaborate, but not Pure, that's because the
    --  functions here such as Line are clearly not pure functions, and normally
@@ -47,6 +53,8 @@ package GNAT.Source_Info is
    --  intrinsics as not Pure, even in Pure units, so no problems arose.
 
    function File return String with
+     Volatile_Function,
+     Global => Source_Code_Information,
      Import, Convention => Intrinsic;
    --  Return the name of the current file, not including the path information.
    --  The result is considered to be a static string constant.
@@ -57,6 +65,8 @@ package GNAT.Source_Info is
    --  static expression.
 
    function Source_Location return String with
+     Volatile_Function,
+     Global => Source_Code_Information,
      Import, Convention => Intrinsic;
    --  Return a string literal of the form "name:line", where name is the
    --  current source file name without path information, and line is the
@@ -66,6 +76,8 @@ package GNAT.Source_Info is
    --  string constant.
 
    function Enclosing_Entity return String with
+     Volatile_Function,
+     Global => Source_Code_Information,
      Import, Convention => Intrinsic;
    --  Return the name of the current subprogram, package, task, entry or
    --  protected subprogram. The string is in exactly the form used for the
@@ -80,15 +92,21 @@ package GNAT.Source_Info is
    --  from within generic templates.
 
    function Compilation_ISO_Date return String with
+     Volatile_Function,
+     Global => Source_Code_Information,
      Import, Convention => Intrinsic;
    --  Returns date of compilation as a static string "yyyy-mm-dd".
 
    function Compilation_Date return String with
+     Volatile_Function,
+     Global => Source_Code_Information,
      Import, Convention => Intrinsic;
    --  Returns date of compilation as a static string "mmm dd yyyy". This is
    --  in local time form, and is exactly compatible with C macro __DATE__.
 
    function Compilation_Time return String with
+     Volatile_Function,
+     Global => Source_Code_Information,
      Import, Convention => Intrinsic;
    --  Returns GMT time of compilation as a static string "hh:mm:ss". This is
    --  in local time form, and is exactly compatible with C macro __TIME__.