1. Forum
  2. Usenet
  3. COMP.LANG.ADA

  • GNAT.Source_Info Volatile and SPARK

    From Kevin Chadwick@21:1/5 to All on Fri Dec 8 18:28:24 2023
    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

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Kevin Chadwick@21:1/5 to Kevin Chadwick on Sat Dec 9 14:33:22 2023
    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

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Kevin Chadwick@21:1/5 to All on Sat Dec 9 15:13:28 2023
    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

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Jeffrey R.Carter@21:1/5 to Kevin Chadwick on Sat Dec 9 15:57:41 2023
    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

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Kevin Chadwick@21:1/5 to All on Sat Dec 9 14:16:17 2023
    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

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)