Re: SPARK 2014 and protected objects

[Shark8 <onewingedshark@gmail.com>]

On Tuesday, August 30, 2016 at 4:33:59 AM UTC-6, Simon Wright wrote:
> 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

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