public inbox for gcc-cvs@sourceware.org help / color / mirror / Atom feed
From: Marc Poulhi?s <dkm@gcc.gnu.org> To: gcc-cvs@gcc.gnu.org Subject: [gcc r13-4361] ada: Annotate GNAT.Source_Info with an abstract state Date: Mon, 28 Nov 2022 12:04:08 +0000 (GMT) [thread overview] Message-ID: <20221128120408.DA47B385B1A5@sourceware.org> (raw) 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__.
reply other threads:[~2022-11-28 12:04 UTC|newest] Thread overview: [no followups] expand[flat|nested] mbox.gz Atom feed
Reply instructions: You may reply publicly to this message via plain-text email using any one of the following methods: * Save the following mbox file, import it into your mail client, and reply-to-all from there: mbox Avoid top-posting and favor interleaved quoting: https://en.wikipedia.org/wiki/Posting_style#Interleaved_style * Reply using the --to, --cc, and --in-reply-to switches of git-send-email(1): git send-email \ --in-reply-to=20221128120408.DA47B385B1A5@sourceware.org \ --to=dkm@gcc.gnu.org \ --cc=gcc-cvs@gcc.gnu.org \ /path/to/YOUR_REPLY https://kernel.org/pub/software/scm/git/docs/git-send-email.html * If your mail client supports setting the In-Reply-To header via mailto: links, try the mailto: linkBe sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).