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!feeder.eternal-september.org!nntp-feed.chiark.greenend.org.uk!ewrotcd!newsfeed.xs3.de!io.xs3.de!news.jacob-sparre.dk!franka.jacob-sparre.dk!pnx.dk!.POSTED.rrsoftware.com!not-for-mail
From: "Randy Brukardt" <randy@rrsoftware.com>
Newsgroups: comp.lang.ada
Subject: Re: SPARK question
Date: Mon, 27 Aug 2018 16:36:59 -0500
Organization: JSA Research & Innovation
Message-ID: <pm1qtr$3ii$1@franka.jacob-sparre.dk>
References: 
 <lyo9dnlx2z.fsf@pushface.org><1ac13606-2603-41d5-b5b7-d7fad27369cf@googlegroups.com>
 <lyk1oblfz7.fsf@pushface.org>
Injection-Date: Mon, 27 Aug 2018 21:36:59 -0000 (UTC)
Injection-Info: franka.jacob-sparre.dk;
 posting-host="rrsoftware.com:24.196.82.226";
	logging-data="3666"; mail-complaints-to="news@jacob-sparre.dk"
X-Priority: 3
X-MSMail-Priority: Normal
X-Newsreader: Microsoft Outlook Express 6.00.2900.5931
X-RFC2646: Format=Flowed; Original
X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.7246
Xref: reader02.eternal-september.org comp.lang.ada:54276
Date: 2018-08-27T16:36:59-05:00
List-Id: <comp.lang.ada>

"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.

                                    Randy.