SPARK 2014 and protected objects

[Simon Wright <simon@pushface.org>]

I'm struggling with a package whose spec has subprograms whose bodies
call a PO declared in the package body, which governs access to volatile
data (an SPI-connected device). gnatprove (2016) wants me to use
Abstract_State and (sometimes) Part_Of, but I can't get the syntax
right. Does anyone have any worked examples?

What I have so far is at http://pastebin.com/HGpH4xL4; the error I get
is

     1. package body PO
     2. with Refined_State => (State => (Protected_Value,
                               |
        >>> non-external state "State" cannot contain external constituents in refinement

     3.                                  Impl))
     4. is
     5.
     6.    Protected_Value : Integer := 0
     7.      with Volatile;
     8.
     9.    protected Impl is
    10.       procedure Set (Value : Integer);
    11.       procedure Get (Value : out Integer);
    12.    end Impl;

If I don't include Impl in the refined state then I get

     1. package body PO
                     |
        >>> body of package "PO" has unused hidden states
        >>> variable "Impl" defined at line 8

     2. with Refined_State => (State => (Protected_Value))
                               |
        >>> non-external state "State" cannot contain external constituents in refinement

     3. is
     4.
     5.    Protected_Value : Integer := 0
     6.      with Volatile;
     7.

(I've looked at AdaCore's Certyflie[1], but it looks as though all the
POs are in packages that they don't prove)

[1] https://github.com/AdaCore/Certyflie