[Spark2014-discuss] Not null access constant in SPARK

Yannick Moy 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;
> 
> begin
>    null;
> 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...
URL: <http://lists.forge.open-do.org/pipermail/spark2014-discuss/attachments/20151104/7ef48adf/attachment.html>


More information about the Spark2014-discuss mailing list