[Spark2014-discuss] Not null access constant in SPARK

Yannick Moy moy at adacore.com
Mon Nov 2 08:59:25 CET 2015


-- Johannes Kanig (2015-11-01)
> Hello David,
> 
> On Mon, 2015-11-02, 6:52:34, David Lesens <david.lesens at orange.fr> wrote:
>> I was wondering why “not null access constant” is not supported in SPARK
>> 2014
>> 
>> Is it because there is a risk with this construct? (I don’t see any risk)
>> 
>> Or is it just because the principle of SPARK is to not support access,
>> even if it is safe
>> In this case, is there any plan for the future of SPARK to support “not
>> null access constant”?
> 
> Indeed, this particular construct is excluded because all uses of "access" are excluded from the SPARK subset. I also do not think there is a risk with this construct. This is certainly something we will consider for future SPAK versions.


Hi David,

As Johannes said, all access types are currently excluded from SPARK, but we're planning to allow some safe access values to SPARK in the future. A "not null access constant" guarantees that the access value cannot be used to modify the underlying value, but this does not prevent the underlying value from being modified, as visible from this example:

procedure NNCA is
   X : aliased Integer := 0;
   A : not null access constant Integer := X'Access;
begin
   pragma Assert (A.all = 0);
   X := 1;
   pragma Assert (A.all = 0);
end NNCA;

The second assertion fails in the code above because the value pointe-to by A has been modified. While it could be possible to deal with such values in SPARK by assuming they can be modified at any moment (treating them like pointers to volatile data), I doubt this would be useful in your case? Would it be the case instead that the value pointed would never change, in the code you're interested in? If so, that would deserve a special aspect/pragma in SPARK to denote pointers to data that cannot be modified. 

I'm curious to know if this would match your need.
--
Yannick Moy, Senior Software Engineer, AdaCore




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.forge.open-do.org/pipermail/spark2014-discuss/attachments/20151102/14fa0ab7/attachment.html>


More information about the Spark2014-discuss mailing list