Re: SPARK 2014 and protected objects

[Simon Wright <simon@pushface.org>]

Shark8 <onewingedshark@gmail.com> writes:

> Have you tried moving "Protected_Value : Integer := 0 with Volatile;"
> into the protected object's private section (inside the
> specification)?

Like this ...

   private

      Protected_Value : Integer := 0
        with Volatile,
        Part_Of => State;

   end PO;

but I still get the problem with Impl ... so I put its spec in po.ads
similarly ... State still needs refinement, but it can't be done ...

     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

What is a non-external state?

(by the way, this is the compiler complaining, not gnatprove)