Re: SPARK question

["Randy Brukardt" <randy@rrsoftware.com>]

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