[Spark2014-discuss] Not null access constant in SPARK

Johannes Kanig kanig at adacore.com
Sun Nov 1 23:35:50 CET 2015

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.



Johannes Kanig, PhD
Senior Software Engineer
<kanig at adacore.com>

More information about the Spark2014-discuss mailing list