* Hiding Code from SPARK
@ 2022-06-04 16:16 Jeffrey R.Carter
0 siblings, 0 replies; only message in thread
From: Jeffrey R.Carter @ 2022-06-04 16:16 UTC (permalink / 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
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
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2022-06-04 16:16 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-06-04 16:16 Hiding Code from SPARK Jeffrey R.Carter
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox