From: Claire Dross <dross@adacore.com>
Date: Fri, 25 Nov 2022 15:28:47 +0000 (+0100)
Subject: ada: Annotate GNAT.Source_Info with an abstract state
X-Git-Tag: basepoints/gcc-14~2846
X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=80ad275cf1e6f308d3bbafc34635eb56851d6862;p=thirdparty%2Fgcc.git

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 --git a/gcc/ada/libgnat/g-souinf.ads b/gcc/ada/libgnat/g-souinf.ads
index 700f5180c825..6b72a6497f13 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__.