From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM autolearn=unavailable autolearn_force=no version=3.4.4 X-Received: by 10.159.35.65 with SMTP id 59mr3193488uae.8.1472568352781; Tue, 30 Aug 2016 07:45:52 -0700 (PDT) X-Received: by 10.157.40.67 with SMTP id h3mr245859otd.6.1472568352740; Tue, 30 Aug 2016 07:45:52 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!usenet.blueworldhosting.com!feeder01.blueworldhosting.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!j37no11643490qta.0!news-out.google.com!n186ni216ith.0!nntp.google.com!x131no1198288ite.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Tue, 30 Aug 2016 07:45:52 -0700 (PDT) In-Reply-To: Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=174.28.146.45; posting-account=lJ3JNwoAAAAQfH3VV9vttJLkThaxtTfC NNTP-Posting-Host: 174.28.146.45 References: User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: Subject: Re: SPARK 2014 and protected objects From: Shark8 Injection-Date: Tue, 30 Aug 2016 14:45:52 +0000 Content-Type: text/plain; charset=UTF-8 Xref: news.eternal-september.org comp.lang.ada:31644 Date: 2016-08-30T07:45:52-07:00 List-Id: 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)?