From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,50137bb64a119cfc X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2003-02-19 18:28:37 PST Path: archiver1.google.com!postnews1.google.com!not-for-mail From: mheaney@on2.com (Matthew Heaney) Newsgroups: comp.lang.ada Subject: Re: "access constant" discriminant Date: 19 Feb 2003 18:28:37 -0800 Organization: http://groups.google.com/ Message-ID: <1ec946d1.0302191828.527e22be@posting.google.com> References: NNTP-Posting-Host: 66.162.65.162 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-Trace: posting.google.com 1045708117 8649 127.0.0.1 (20 Feb 2003 02:28:37 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: 20 Feb 2003 02:28:37 GMT Xref: archiver1.google.com comp.lang.ada:34244 Date: 2003-02-20T02:28:37+00:00 List-Id: rod.chapman@praxis-cs.co.uk (Rod Chapman) wrote in message news:... > tmoran@acm.org wrote in message news:... > > 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?