Rocksolid Light

Welcome to RetroBBS

mail  files  register  newsreader  groups  login

Message-ID:  

Extreme feminine beauty is always disturbing. -- Spock, "The Cloud Minders", stardate 5818.4

devel / comp.lang.ada / GNAT.Source_Info Volatile and SPARK

SubjectAuthor
* GNAT.Source_Info Volatile and SPARKKevin Chadwick
`* Re: GNAT.Source_Info Volatile and SPARKKevin Chadwick
 `* Re: GNAT.Source_Info Volatile and SPARKKevin Chadwick
  `* Re: GNAT.Source_Info Volatile and SPARKJeffrey R.Carter
   `- Re: GNAT.Source_Info Volatile and SPARKKevin Chadwick

1
GNAT.Source_Info Volatile and SPARK

<ukvn87$1r9gq$1@dont-email.me>

  copy mid

https://www.rocksolidbbs.com/devel/article-flat.php?id=10291&group=comp.lang.ada#10291

  copy link   Newsgroups: comp.lang.ada
Path: i2pn2.org!i2pn.org!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: kc-usenet@chadwicks.me.uk (Kevin Chadwick)
Newsgroups: comp.lang.ada
Subject: GNAT.Source_Info Volatile and SPARK
Date: Fri, 8 Dec 2023 18:28:24 -0000 (UTC)
Organization: A noiseless patient Spider
Lines: 17
Message-ID: <ukvn87$1r9gq$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Fri, 8 Dec 2023 18:28:24 -0000 (UTC)
Injection-Info: dont-email.me; posting-host="416a53f25687c8ca32bfa777936870fc";
logging-data="1943066"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+/Tc1wvDUROKaS0zgRopfR3c/5D+7n8A8="
User-Agent: PhoNews/3.13.2 (Android/13)
Cancel-Lock: sha1:zfNJ+rYkI7eT0JdmHOsEcR6uu60=
 by: Kevin Chadwick - Fri, 8 Dec 2023 18:28 UTC

I guess the SPARK annotations in GNAT.Source_Info mark them as
Volatile_Functions for good reason.

I'm not sure how to handle using them in SPARK. They produce compile time
known constants but I guess SPARK does not know e.g. the String length.

I use them in a logging function which is everywhere. So I get error
Volatile function call as actual is not allowed in SPARK when calling
GNAT.Source_Info.Source_Location as a loggers parameter. Perhaps I should
just avoid using them for SPARK compatibility? I can get by with
GNAT.Source_Info.Line which only produces warnings and not the above error
but it is not ideal.

I can use the function File as a package global constant. Any other ideas?

--
Regards, Kc

Re: GNAT.Source_Info Volatile and SPARK

<ul1srg$27ssd$1@dont-email.me>

  copy mid

https://www.rocksolidbbs.com/devel/article-flat.php?id=10292&group=comp.lang.ada#10292

  copy link   Newsgroups: comp.lang.ada
Path: i2pn2.org!i2pn.org!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: kc-usenet@chadwicks.me.uk (Kevin Chadwick)
Newsgroups: comp.lang.ada
Subject: Re: GNAT.Source_Info Volatile and SPARK
Date: Sat, 9 Dec 2023 14:16:17 -0000 (UTC)
Organization: A noiseless patient Spider
Lines: 10
Message-ID: <ul1srg$27ssd$1@dont-email.me>
References: <ukvn87$1r9gq$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Sat, 9 Dec 2023 14:16:17 -0000 (UTC)
Injection-Info: dont-email.me; posting-host="f6e9be193d3e804a84a12316ab678d7e";
logging-data="2356109"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/4yFxqXLZ/4hLxv0/W/m3MVRM2cWsystA="
User-Agent: PhoNews/3.13.2 (Android/13)
Cancel-Lock: sha1:J5s1nusSK+r2o6Ih8Vh61tOnfYw=
In-Reply-To: <ukvn87$1r9gq$1@dont-email.me>
 by: Kevin Chadwick - Sat, 9 Dec 2023 14:16 UTC

>I can use the function File as a package global constant. Any other ideas?

I shall go with doing the above per package for Gnat.Source_Info.File and
wrapping the Gnat.Source_Info.Line procedure with one marked with Global =>
null.

Where would I suggest that Global => null be added to Line?

--
Regards, Kc

Re: GNAT.Source_Info Volatile and SPARK

<ul1tri$28240$1@dont-email.me>

  copy mid

https://www.rocksolidbbs.com/devel/article-flat.php?id=10293&group=comp.lang.ada#10293

  copy link   Newsgroups: comp.lang.ada
Path: i2pn2.org!i2pn.org!news.niel.me!news.gegeweb.eu!gegeweb.org!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: kc-usenet@chadwicks.me.uk (Kevin Chadwick)
Newsgroups: comp.lang.ada
Subject: Re: GNAT.Source_Info Volatile and SPARK
Date: Sat, 9 Dec 2023 14:33:22 -0000 (UTC)
Organization: A noiseless patient Spider
Lines: 13
Message-ID: <ul1tri$28240$1@dont-email.me>
References: <ukvn87$1r9gq$1@dont-email.me> <ul1srg$27ssd$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Sat, 9 Dec 2023 14:33:22 -0000 (UTC)
Injection-Info: dont-email.me; posting-host="f6e9be193d3e804a84a12316ab678d7e";
logging-data="2361472"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1892+qvVyUusNfi8wasf99spYGsoULnwKw="
User-Agent: PhoNews/3.13.2 (Android/13)
Cancel-Lock: sha1:cIqFs/4x8/WBS0New5J0AD0wvf8=
In-Reply-To: <ul1srg$27ssd$1@dont-email.me>
 by: Kevin Chadwick - Sat, 9 Dec 2023 14:33 UTC

On 09/12/2023 14:16, Kevin Chadwick wrote:
>>I can use the function File as a package global constant. Any other ideas?
>
>I shall go with doing the above per package for Gnat.Source_Info.File and
> wrapping the Gnat.Source_Info.Line procedure with one marked with Global =>
> null.
>
>Where would I suggest that Global => null be added to Line?

Doh...Of course I can't wrap Line, ha ha. If I want the right line.

--
Regards, Kc

Re: GNAT.Source_Info Volatile and SPARK

<ul1v95$2735i$1@dont-email.me>

  copy mid

https://www.rocksolidbbs.com/devel/article-flat.php?id=10294&group=comp.lang.ada#10294

  copy link   Newsgroups: comp.lang.ada
Path: i2pn2.org!i2pn.org!usenet.goja.nl.eu.org!weretis.net!feeder8.news.weretis.net!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: spam.jrcarter.not@spam.acm.org.not (Jeffrey R.Carter)
Newsgroups: comp.lang.ada
Subject: Re: GNAT.Source_Info Volatile and SPARK
Date: Sat, 9 Dec 2023 15:57:41 +0100
Organization: A noiseless patient Spider
Lines: 29
Message-ID: <ul1v95$2735i$1@dont-email.me>
References: <ukvn87$1r9gq$1@dont-email.me> <ul1srg$27ssd$1@dont-email.me>
<ul1tri$28240$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Sat, 9 Dec 2023 14:57:42 -0000 (UTC)
Injection-Info: dont-email.me; posting-host="333748014917dd824f52bf756196e0b4";
logging-data="2329778"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX187CjGN9u7z1ieeOP++arMAJ6hn7272kt4="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:juoHxH0hz81KLI6rR1BfEnmvMuY=
In-Reply-To: <ul1tri$28240$1@dont-email.me>
Content-Language: en-US
 by: Jeffrey R.Carter - Sat, 9 Dec 2023 14:57 UTC

On 2023-12-09 15:33, Kevin Chadwick wrote:
> On 09/12/2023 14:16, Kevin Chadwick wrote:
>>
>> I shall go with doing the above per package for Gnat.Source_Info.File and
>> wrapping the Gnat.Source_Info.Line procedure with one marked with Global =>
>> null.
>
> Doh...Of course I can't wrap Line, ha ha. If I want the right line.

Perhaps

private with Gnat.Source_Info;

package Source_Line_Info with SPARK_Mode is
function Line ... with Global => null;
private -- Source_Line_Info
pragma SPARK_Mode (Off);

function Line ... renames Gnat.Source_Info.line;
end Source_Line_Info;

(Untested)

--
Jeff Carter
"Unix and C are the ultimate computer viruses."
Richard Gabriel
99

Re: GNAT.Source_Info Volatile and SPARK

<ul206o$28dqn$1@dont-email.me>

  copy mid

https://www.rocksolidbbs.com/devel/article-flat.php?id=10295&group=comp.lang.ada#10295

  copy link   Newsgroups: comp.lang.ada
Path: i2pn2.org!i2pn.org!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: kc-usenet@chadwicks.me.uk (Kevin Chadwick)
Newsgroups: comp.lang.ada
Subject: Re: GNAT.Source_Info Volatile and SPARK
Date: Sat, 9 Dec 2023 15:13:28 -0000 (UTC)
Organization: A noiseless patient Spider
Lines: 22
Message-ID: <ul206o$28dqn$1@dont-email.me>
References: <ukvn87$1r9gq$1@dont-email.me> <ul1srg$27ssd$1@dont-email.me>
<ul1tri$28240$1@dont-email.me> <ul1v95$2735i$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Sat, 9 Dec 2023 15:13:28 -0000 (UTC)
Injection-Info: dont-email.me; posting-host="f6e9be193d3e804a84a12316ab678d7e";
logging-data="2373463"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/vrO/JAtkPU3LcgSZyVn5exSlZ9Z8R50g="
User-Agent: PhoNews/3.13.2 (Android/13)
Cancel-Lock: sha1:pD0Q10uNzQxNm68XqRTQsxP8iCE=
In-Reply-To: <ul1v95$2735i$1@dont-email.me>
 by: Kevin Chadwick - Sat, 9 Dec 2023 15:13 UTC

>> Doh...Of course I can't wrap Line, ha ha. If I want the right line.
>
>Perhaps
>
>private with Gnat.Source_Info;
>
>package Source_Line_Info with SPARK_Mode is
> function Line ... with Global => null;
>private -- Source_Line_Info
> pragma SPARK_Mode (Off);
>
> function Line ... renames Gnat.Source_Info.line;
>end Source_Line_Info;
>
>(Untested)

Interesting, Thanks. I might just use random identifiers. With the added
benefit of knowing it will work with any runtime, any platform and any
compilation options.

--
Regards, Kc

1
server_pubkey.txt

rocksolid light 0.9.8
clearnet tor