Re: SPARK question

[Simon Wright <simon@pushface.org>]

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