[Spark2014-discuss] Not null access constant in SPARK

David Lesens david.lesens at orange.fr
Tue Nov 3 22:14:19 CET 2015


On 02/11/2015 08:59, Yannick Moy wrote:
> -- Johannes Kanig (2015-11-01)
>> Hello David,
>>
>> On Mon, 2015-11-02, 6:52:34, David Lesens <david.lesens at orange.fr
>> <mailto: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.

Thanks for your answer

Indeed, in my case, I am using a pointer to a constant just to avoid
useless copies of data

Neither the pointer or the data on which the pointer points can be modified

So, your "special aspect/pragma" may solve this problem



More information about the Spark2014-discuss mailing list