Re: SPARK 2014 and protected objects

[Simon Wright <simon@pushface.org>]

Shark8 <onewingedshark@gmail.com> writes:

>> I had Protected_Value outside the PO because it's standing in for a
>> number of I/O registers communicating with devices on a shared SPI
>> bus via their /Chip Select lines. Not sure how to deal with the
>> concept of "a number of machine registers"!
>
> Well, if they're memory-mapped registers you could use something like:
> Regester_A : Word with Address => Location;

I meant rather how I was to get SPARK to handle them. I suppose one
could detail each individual register or even bit field, but as far as I
can see most folk just turn SPARK_Mode off.