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=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: Simon Wright <simon@pushface.org>
Newsgroups: comp.lang.ada
Subject: Re: SPARK question
Date: Tue, 28 Aug 2018 20:05:55 +0100
Organization: A noiseless patient Spider
Message-ID: <ly8t4ql3ak.fsf@pushface.org>
References: <lyo9dnlx2z.fsf@pushface.org>
	<1ac13606-2603-41d5-b5b7-d7fad27369cf@googlegroups.com>
	<lyk1oblfz7.fsf@pushface.org> <pm1qtr$3ii$1@franka.jacob-sparre.dk>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: reader02.eternal-september.org;
 posting-host="dc220bad8cc6392293fad97f6df5b436";
	logging-data="20129"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX18My/ObGNlPWI/oNFQEy2HzXvu08xxaktc="
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.3 (darwin)
Cancel-Lock: sha1:7ZdpkHfycybYTz7++MpkZoLqxKg=
	sha1:HXsOGtcRjLpoVZhzYhXjdl0BTYA=
Xref: reader02.eternal-september.org comp.lang.ada:54284
Date: 2018-08-28T20:05:55+01:00
List-Id: <comp.lang.ada>

"Randy Brukardt" <randy@rrsoftware.com> writes:

> "Simon Wright" <simon@pushface.org> wrote in message 
> news:lyk1oblfz7.fsf@pushface.org...
>> Shark8 <onewingedshark@gmail.com> writes:
>>
>>> On Monday, August 27, 2018 at 8:10:13 AM UTC-6, Simon Wright wrote:
>>>> With SPARK CE 2018, I'm seeing
>>>>
>>>>    commander.ads:103:08: high: "memory accessed through objects of
>>>>    access type" must be a global Output of "Commander_Watchdog"
>>>>
>>>> Google tells me nothing, any clues here? (and, obvs, where _should_
>>>> I be asking?)
>>>
>>> I think it's saying that you need a "Global" aspect on
>>> "Commander_Watchdog", see
>>> https://blog.adacore.com/spark-2014-rationale-data-dependencies -- in
>>> particular:
>>>
>>>    procedure Add (X, Y : in Integer) with
>>>      Global => (Output => Global_Variable);
>>
>> Yes, but! similar messages say e.g.
>>
>>   commander.ads:103:08: high: "Current_System_Status" must be a global
>>   Output of "Commander_Watchdog"
>>
>> and I can't see any "objects of access type" used in
>> Commander_Watchdog.
>
> I'd guess that it comes from some dereference, and that might be in
> some subprogram that you called. (But I'm reasoning from the proposed
> Ada 2020 rules and not the slightly different SPARK rules.) It's also
> possible that some Ada feature you used is internally implemented with
> an access type, but I wouldn't have expected SPARK to pick that up.

I think you must be right. I had thought that gnatprove would choke on
any use of 'access', this is clearly not so (now).