[Spark2014-discuss] Not null access constant in SPARK
moy at adacore.com
Wed Nov 4 08:49:39 CET 2015
-- Hugues Jérôme (2015-11-03)
> I’m curious wether Ada 2012 (or even 2005) already has a solution, one can have (as accepted by GPL 2015)
> procedure Foo is
> type Bar is not null access constant Integer;
> I1: aliased constant Integer := 10;
> Bar_C : constant Bar := I1'Access;
> end Foo;
> I have the felling this match David’s requirement, without need to special pragma. I may be abusing “contant" though
> Bar_C is a point that cannot be modified (constant) to a integer that cannot be modified as well (as far as I understand the Ada RM, but I’m not that familiar to those "new" features as I’m restricting myself from using pointers).
> Any thoughts ?
That's clever! Indeed, that would be suitable for formal analysis, as the analysis can reliably consider that Bar_C.all is always aliased to I1, which is constant.
I wonder if that's not too restricted for your usage David? Would you be able to declare a constant like I1 in Jérôme's example, or would it be a variable that is constant after some point? In it's the latter, we may also consider variables that are Constant_After_Elaboration (as defined in SPARK, see http://docs.adacore.com/spark2014-docs/html/ug/spark_2014.html#aspect-constant-after-elaboration <http://docs.adacore.com/spark2014-docs/html/ug/spark_2014.html#aspect-constant-after-elaboration>) instead of only constants.
Yannick Moy, Senior Software Engineer, AdaCore
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Spark2014-discuss