Re: SPARK 2014 and protected objects

[Simon Wright <simon@pushface.org>]

Shark8 <onewingedshark@gmail.com> writes:

>    protected Impl
>      with Part_Of => State
>    is
>       procedure Set (Value : Integer)
>         with Depends => ((Impl =>+ Value));
>       procedure Get (Value : out Integer)
>         with Depends => (Impl => Impl, Value => Impl);
>
>    private
> 	Protected_Value : Integer := 0;
>    end Impl;
>     
>     -- GNAT doesn't allow Volatile on the protected object's with.
>     Pragma Volatile(Impl);

We seem to have come up with (almost) the same solution, which gives me
confidence it's the right one. Thanks.

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