[Spark2014-discuss] Not null access constant in SPARK
kanig at adacore.com
Sun Nov 1 23:35:50 CET 2015
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
> 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