Re: SPARK 2014 and protected objects

[Shark8 <onewingedshark@gmail.com>]

On Wednesday, August 31, 2016 at 2:55:42 PM UTC-6, Simon Wright wrote:
> Shark8 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.

Well, Randy just pointed out that specifying the address was/is meant for registers -- https://groups.google.com/forum/#!topic/comp.lang.ada/gPJh0r2XxcA -- so I guess it just depends on how far you want to use SPARK on them.