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, WEIRD_PORT autolearn=unavailable autolearn_force=no version=3.4.4 X-Received: by 10.43.70.132 with SMTP id yg4mr5582276icb.30.1404415760611; Thu, 03 Jul 2014 12:29:20 -0700 (PDT) X-Received: by 10.140.95.244 with SMTP id i107mr9826qge.39.1404415760576; Thu, 03 Jul 2014 12:29:20 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!usenet.blueworldhosting.com!feeder01.blueworldhosting.com!peer02.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!i13no5712329qae.1!news-out.google.com!a8ni6410qaq.1!nntp.google.com!w8no5716545qac.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Thu, 3 Jul 2014 12:29:20 -0700 (PDT) Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=90.219.105.227; posting-account=qa2LvwoAAADwbTxJVBI5rHWSlh3aClXp NNTP-Posting-Host: 90.219.105.227 User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: Subject: SPARK 2014 Abstract_State visibility rules with generic packages From: daniel.dmk@googlemail.com Injection-Date: Thu, 03 Jul 2014 19:29:20 +0000 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Received-Bytes: 6206 X-Received-Body-CRC: 1131228303 Xref: news.eternal-september.org comp.lang.ada:20697 Date: 2014-07-03T12:29:20-07:00 List-Id: Hi All, I'm having trouble with visibility rules in GNAT with Abstract_State in a g= eneric package. Specifically, this package is used as a argument to another= generic package. I've cut down my code into a small example that demonstrates my problem. He= re's my problem in a nutshell: I have the following generic package G1 which defines some abstract externa= l state, as in SPARK 2014 LRM 7.1.3 and 7.1.4, and defines a procedure that= uses this abstract state in Globals and Depends aspects: generic Base_Address : Natural; package G1 with Abstract_State =3D> (Register with External =3D> Async_Writers) is =20 procedure Read_Register(Value : out Natural) with Global =3D> (Input =3D> Register), Depends =3D> (Value =3D> Register); =20 end G1; Next, I use this package as a generic package parameter in another package = as follows: with G1; generic with package Regs is new G1(<>); package G2 is procedure Foo(Value : out Natural); end G2; =20 However, the "with package" clause in G2 generates an error in GNAT, compla= ining that "Register" in G1 is not visible when the package is instantiated= in G2. Specifically, the error messages are: g2.ads:4:04: instantiation error at g1.ads:8 g2.ads:4:04: "Register" is not visible (more references follow) g2.ads:4:04: instantiation error at g1.ads:8 g2.ads:4:04: non-visible declaration at g1.ads:4 =20 Can anyone provide some insight as to why the "Register" abstract state in = G1 is not visible in the generic part of G2? =20 Being fairly new to Ada and SPARK, I don't fully understand the visibility = rules so I guess I'm doing something illegal here but I don't quite underst= and what. I've been reading the Ada 2012 LRM and SPARK 2014 LRM to try and = understand what is going on here. Section 7.1.4 of the SPARK 2014 LRM state= s: "State abstraction provides a mechanism for naming, in a package's visib= le part, state (typically a collection of variables) that will be declared = within the package's body (its hidden state)." =20 So the abstract state "Register" should be in the package's visible part as= far as I can tell. And indeed, I can instantiate G1 as normal and then cal= l Read_Register: declare package X is new G1(16#4000_0000#); -- OK Value : Natural; begin X.Read_Register(Value); -- OK end =20 =20 I'll provide some more insight as to what I am doing (perhaps there is a be= tter way to do what I am trying to do). Essentially, I am writing some code in SPARK 2014 to interface with memory-= mapped peripheral registers on a microcontroller (STM32 F4 series). For som= e peripherals, there are several instances of the peripheral, for example, = there are up to 11 GPIO peripherals (GPIO A .. K), each with the same regis= ter layout. In this case, I want to be able to define the layout of the reg= isters, and then use this "template" to define each peripheral.=20 A key point here is that I wish to use the "external state" features of SPA= RK 2014 (LRM 7.1.2) with the Async_Writers, Async_Readers, Effective_Writes= , and Effective_Reads aspects in order to aid flow analysis. Each register = in the peripheral can have different combinations of these aspects, and the= se aspects can only be applied to volatile *objects*. Hence, I cannot simpl= y define a record containing all these registers (with the relevant aspects= ) because I would be unable to assign these aspects to each register inside= the record. They can only be applied to the global volatile objects. For this reason, I am using a generic package (like my example package G1 a= bove) to define registers (which are hidden in the package body) along with= accessor procedures to ensure that those registers are accessed correctly.= I can then assign the external state aspects to each of the registers (i.e= . global objects), and simply instantiate the generic package for each of t= he peripherals at their address. For example, using my package G1 from abov= e: with G1; package Registers is -- Instantiate some registers package R1 is new G1(16#3000_0000#); package R2 is new G1(16#4000_0000#); package R3 is new G1(16#5000_0000#); package R4 is new G1(16#6000_0000#); package R5 is new G1(16#7000_0000#); end Registers; =20 Next, I would like to create a package containing some higher-level functio= nality. For example, to configure a GPIO. I would like for these procedures= to be able to operate on any of the GPIOs, so I have defined the package a= s a generic package (like my example in G2, above) so that I can instantiat= e it like so: package R1_Functions is new G2(Registers.R1); package R2_Functions is new G2(Registers.R2); -- etc =20 However, I'm running into the problem with the visibility. Perhaps there is a better way to achieve what I'm after? Regards, Daniel