Q: SPARK visibility rules and inherit annotations.
in [ADA]
|
From: Peter C. Chapin on 19 May 2010 11:04 I'm working on a SPARK program. Right now I'm just doing design so my focus is on package specifications; there are no package bodies. I'm having some trouble with the following: with TMLib.Cryptographic_Services; --# inherit TMLib.Cryptographic_Services; package TMLib.Credentials is type Credential_Type is private; -- Converts the raw bytes of a certificate transfer format to a credential. procedure Certificate_To_Credential (Raw_Data : in TMLib.Cryptographic_Services.Octet_Array; Credential : out Credential_Type; Valid : out Boolean); --# derives Credential from Raw_Data & --# Valid from Raw_Data; -- Other stuff not shown here... end TMLib.Credentials; The SPARK Examiner complains about the use of "Cryptographic_Services" in the declaration of the Raw_Data parameter to the procedure. Specifically I get error 754 that says (roughly) "The identifier Cryptographic_Services is not declared or not visible." I am then told that I probably need both a 'with' statement in the context clause and an 'inherit' annotation. Don't I have those things? Note that TMLib.Cryptographic_Services examines without error but it does generate a warning because the private section is empty and currently hidden from SPARK with a 'hide' annotation. It seems unlikely to me that has anything to do with my problem. Note that TMLib.Cryptographic_Services is a public child of TMLib. I tried adding a 'with TMLib;' in the context clause but that didn't have any effect. I realize the problem is probably something silly but I'm a bit baffled here. Any pointers would be appreciated. Thanks! Peter
From: Phil Thornley on 19 May 2010 11:54 On 19 May, 16:04, "Peter C. Chapin" <pcc482...(a)gmail.com> wrote: > I'm working on a SPARK program. Right now I'm just doing design so my focus is > on package specifications; there are no package bodies. I'm having some > trouble with the following: > > with TMLib.Cryptographic_Services; > > --# inherit TMLib.Cryptographic_Services; > package TMLib.Credentials is > type Credential_Type is private; > > -- Converts the raw bytes of a certificate transfer format to a credential. > procedure Certificate_To_Credential > (Raw_Data : in TMLib.Cryptographic_Services.Octet_Array; > Credential : out Credential_Type; > Valid : out Boolean); > --# derives Credential from Raw_Data & > --# Valid from Raw_Data; > > -- Other stuff not shown here... > end TMLib.Credentials; > > The SPARK Examiner complains about the use of "Cryptographic_Services" in the > declaration of the Raw_Data parameter to the procedure. Specifically I get > error 754 that says (roughly) "The identifier Cryptographic_Services is not > declared or not visible." I am then told that I probably need both a 'with' > statement in the context clause and an 'inherit' annotation. Don't I have > those things? > > Note that TMLib.Cryptographic_Services examines without error but it does > generate a warning because the private section is empty and currently hidden > from SPARK with a 'hide' annotation. It seems unlikely to me that has > anything to do with my problem. Note that TMLib.Cryptographic_Services is a > public child of TMLib. > > I tried adding a 'with TMLib;' in the context clause but that didn't have any > effect. I realize the problem is probably something silly but I'm a bit > baffled here. Any pointers would be appreciated. > > Thanks! > > Peter Peter, The problem comes from the reference in one child of TMLib to another child of TMLib. Where this is the case, in the code and annotations - but not in the inherit or context clauses - the common parent must not appear in the name. So change the line: (Raw_Data : in TMLib.Cryptographic_Services.Octet_Array; to: (Raw_Data : in Cryptographic_Services.Octet_Array; This comes from the rule that no entity in a SPARK program can have more than one name - and in the Ada this type can be called either TMLib.Cryptographic_Services.Octet_Array or Cryptographic_Services.Octet_Array. In SPARK the decision was to enforce the second of these. (I'm sure that this is one error message that could be improved...) Cheers, Phil
From: Yannick Duchêne (Hibou57) on 19 May 2010 12:22 Le Wed, 19 May 2010 17:04:05 +0200, Peter C. Chapin <pcc482719(a)gmail.com> a écrit: > I'm working on a SPARK program. Right now I'm just doing design so my > focus is > on package specifications; there are no package bodies. I'm having some > trouble with the following: > > with TMLib.Cryptographic_Services; > > --# inherit TMLib.Cryptographic_Services; > package TMLib.Credentials is > type Credential_Type is private; > > -- Converts the raw bytes of a certificate transfer format to a > credential. > procedure Certificate_To_Credential > (Raw_Data : in TMLib.Cryptographic_Services.Octet_Array; > Credential : out Credential_Type; > Valid : out Boolean); > --# derives Credential from Raw_Data & > --# Valid from Raw_Data; > > -- Other stuff not shown here... > end TMLib.Credentials; > > The SPARK Examiner complains about the use of "Cryptographic_Services" > in the > declaration of the Raw_Data parameter to the procedure. Specifically I > get > error 754 that says (roughly) "The identifier Cryptographic_Services is > not > declared or not visible." I am then told that I probably need both a > 'with' > statement in the context clause and an 'inherit' annotation. Don't I have > those things? Hi Peter :) I could find something interesting, experimentally. I you use âCryptographic_Services.Octet_Arrayâ instead of âTMLib.Cryptographic_Services.Octet_Arrayâ, this will probably work, as it worked for me. Here is what I did: -- ---------------------------------------------------------------- package TMLib is -- Empty root package. end TMLib; -- ---------------------------------------------------------------- package TMLib.Cryptographic_Services is type Octet_Array is private; private type Octet_Array is range 0 .. 1; -- Dummy type for test purpose. end TMLib.Cryptographic_Services; -- ---------------------------------------------------------------- with TMLib.Cryptographic_Services; --# inherit TMLib.Cryptographic_Services; package TMLib.Credentials is type Credential_Type is private; -- Converts the raw bytes of a certificate transfer -- format to a credential. procedure Certificate_To_Credential (Raw_Data : in Cryptographic_Services.Octet_Array; Credential : out Credential_Type; Valid : out Boolean); --# derives Credential from Raw_Data & --# Valid from Raw_Data; private type Credential_Type is range 0 .. 1; -- Dummy type for test purpose. end TMLib.Credentials; It seems to expect the path to the package to be expressed explicitly as a path in a child package hierarchy. Now will have to look to the reference about it, as I don't remember about this kind of detail anywhere. Note: I still get warnings with the above (some because information flow analysis was enabled) Is it OK for you that ? -- There is even better than a pragma Assert: a SPARK --# check. Wanted: if you know about some though in the area of comparisons between SPARK and VDM, please, let me know. Will enjoy to talk with you about it..
From: Gavino on 19 May 2010 16:41 "Yannick Duch�ne (Hibou57)" <yannick_duchene(a)yahoo.fr> wrote in message news:op.vcynrvxnule2fv(a)garhos... >It seems to expect the path to the package to be expressed explicitly as a >path in a child package hierarchy. Now will have to look to the reference >about it, as I don't remember about this kind of detail anywhere. See end of Section 7.1.1 of the SPARK Reference Manual: "A child package is denoted by a direct name at places where its declaration is directly visible."
From: Peter C. Chapin on 19 May 2010 17:29 Phil Thornley wrote: > Peter, > > The problem comes from the reference in one child of TMLib to another > child of TMLib. > > Where this is the case, in the code and annotations - but not in the > inherit or context clauses - the common parent must not appear in the > name. > > So change the line: > (Raw_Data : in TMLib.Cryptographic_Services.Octet_Array; > to: > (Raw_Data : in Cryptographic_Services.Octet_Array; That did the trick, thanks. Now that you mention it, I seem to recall this coming up for me before, although it was a while ago now. Thanks for your explanation as well. One thing I like about Ada in general is how you can express a design in package specifications and then let the compiler check a few things about its consistency before embarking on the implementation. With SPARK that effect is even greater. For example in my Cryptographic_Services package the Examiner initially complained about how there was no way to initialize one of my private types. It was an oversight on my part (I was missing a critical operation). I would have figured it out eventually, I'm sure, but it was nice to have the issue caught earlier rather than later. It made me reflect on what I was really trying to accomplish with the package and that can only be a good thing. Peter
|
Next
|
Last
Pages: 1 2 Prev: Code Statement Next: SPARK reserved and predefined words : alternative choices |