help / color / mirror / Atom feed
From: "Jeffrey R.Carter" <>
Subject: Hiding Code from SPARK
Date: Sat, 4 Jun 2022 18:16:57 +0200	[thread overview]
Message-ID: <t7g0hr$usi$> (raw)

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

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

                 reply	other threads:[~2022-06-04 16:16 UTC|newest]

Thread overview: [no followups] expand[flat|nested]  mbox.gz  Atom feed
replies disabled

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox