From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on
	ip-172-31-65-14.ec2.internal
X-Spam-Level: *
X-Spam-Status: No, score=1.1 required=3.0 tests=AC_FROM_MANY_DOTS,BAYES_00,
	T_SCC_BODY_TEXT_LINE,WEIRD_PORT autolearn=no autolearn_force=no
	version=3.4.6
Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: "Jeffrey R.Carter" <spam.jrcarter.not@spam.acm.org.not>
Newsgroups: comp.lang.ada
Subject: Hiding Code from SPARK
Date: Sat, 4 Jun 2022 18:16:57 +0200
Organization: A noiseless patient Spider
Message-ID: <t7g0hr$usi$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Sat, 4 Jun 2022 16:16:59 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="cb74c7118f1df89c5993cde4818ea083";
	logging-data="31634"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1/nFysIeNZZ0BOFnYQD0TqzA9U1F+eTniQ="
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:91.0) Gecko/20100101
 Thunderbird/91.9.1
Cancel-Lock: sha1:xA0abhtVVqrBS0xGD0E63WeXFD0=
Content-Language: en-US
Xref: reader02.eternal-september.org comp.lang.ada:63927
List-Id: <comp.lang.ada>

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
is
    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
    is
       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
14