• Hiding Code from SPARK

    From Jeffrey R.Carter@21:1/5 to All on Sat Jun 4 18:16:57 2022
    I've been playing with trying to create a safe-pointer type for SPARK, where SPARK doesn't know that access types are involved. So I've tried

    private with Ada.Finalization;

    generic -- SRC.Pointers
    type Object (<>) is private;
    package SRC.Pointers with SPARK_Mode
    type Pointer is tagged private with
    Default_Initial_Condition => Pointer.Is_Null;

    function Is_Null ...


    private -- SRC.Pointers
    pragma SPARK_Mode (Off);

    type Safe_Group;

    type Name is access Safe_Group;

    type Pointer is new Ada.Finalization.Controlled with record
    Ptr : Name;
    end record;

    overriding procedure Adjust (Item : in out Pointer);
    overriding procedure Finalize (Item : in out Pointer);
    end SRC.Pointers;

    My understanding is that SPARK will not look at the private part or the body. All proofs will assume that the operations are correct.

    When I instantiate it in a SPARK unit:

    package Pointers is new SRC.Pointers (Object => Fixed);

    and run

    gnatprove --level=4 -Psrc

    I get errors such as

    value Off was set for SPARK_Mode on "Adjust" at src-pointers.ads:24

    implying that SPARK is looking at the private part of SRC.Pointers. I can work around that by putting the instantiation in an internal pkg with SPARK_Mode => Off:

    package SPARK_Control with SPARK_Mode => Off
    package Pointers is new SRC.Pointers (Object => Fixed);
    end SPARK_Control;

    package Pointers renames SPARK_Control.Pointers;

    but then I get errors such as

    "Pointer" is not allowed in SPARK

    "Object" is not allowed in SPARK

    which don't make much sense. How can I get SPARK to ignore the private part and body of SRC.Pointers?

    Jeff Carter
    "You cheesy lot of second-hand electric donkey-bottom biters."
    Monty Python & the Holy Grail

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