Re: "access constant" discriminant

[mheaney@on2.com (Matthew Heaney)]

rod.chapman@praxis-cs.co.uk (Rod Chapman) wrote in message news:<cf2c6063.0302101427.51b50e12@posting.google.com>...
> tmoran@acm.org wrote in message news:<lnJ1a.50689$SD6.3473@sccrnsc03>...
> > Can this be done?  How?
> 
> A great shame that it can't.  From the viewpoint of a static analysis
> tool, this is dreadful, since access parameters don't specify whether
> the referenced objected is intended to be referenced, updated, or both - this
> severely limits our ability to do information flow analysis in the presence
> of access parameters, which needs
> such information to be available as part of a subprogram's specifiction
> if it to used usefully and efficiently implemented.  In light of this, SPARK
> currently excludes access parameters.


Realize that what the spec says about subprogram parameter modes is
largely irrelevent in Ada.  If the type is limited, then the Rosen
Trick can be used to get a variable view of the object, no matter what
the spec says.

How does SPARK handle the Rosen Trick?