GNAT.Source_Info Volatile and SPARK

GNAT.Source_Info Volatile and SPARK

[Kevin Chadwick]

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

[Kevin Chadwick]

>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

[Kevin Chadwick]

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

[Jeffrey R.Carter]

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

[Kevin Chadwick]

\r>> 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