SPARK syntax and “use type” : lack of feature ?
in [ADA]
|
Prev: Ada-Belgium Spring 2010 Event, registration deadline approaching
Next: Emacs and long file names
From: Yannick Duchêne (Hibou57) on 24 May 2010 14:41 Hi, I meet a strange behavior with the SPARK syntax checker (via the examiner). If I have something of the form procedure My_Procedure is Who_Know_What : Who_Know_What_Type; use type My_Type; begin ... bla-bla-bla ... end My_Procedure; it's OK. While if I have something like procedure My_Procedure is use type My_Type; begin ... bla-bla-bla ... end My_Procedure; Then the spark syntax checker complains âSyntax Error reserved "IS" cannot be followed by "USE" here.â So, if the âuse typeâ comes after any kind of declaration (type or entity), that's OK, but if this comes at the first place, or worst, alone, so that it cannot be anywhere than at the first place, then it is rejected. Strange. So much strange to me that I wonder if weither or not this is something which had not been seen as a possible issue. What people here think about it ? Is SPARK missing something or is there a rational ?
From: Phil Thornley on 24 May 2010 19:01 On 24 May, 19:41, Yannick Duchêne (Hibou57) <yannick_duch...(a)yahoo.fr> wrote: > Hi, > > I meet a strange behavior with the SPARK syntax checker (via the examiner). I can't get the behaviour that you are reporting (I'm still on GPL version 8.1.1) - can you post a complete SPARKable example? > If I have something of the form > > procedure My_Procedure > is > Who_Know_What : Who_Know_What_Type; > use type My_Type; > begin > ... bla-bla-bla ... > end My_Procedure; > > it's OK. This definitely should not be OK, 'use type' clauses should (normally) only appear as part of a context clause. With this code in a package body: type A_Type is range 1 .. 10; procedure My_Procedure(A : in A_Type; B : in A_Type; X : out Integer) --# derives X from A, B; is Y : Integer; use type A_Type; begin Y := Integer(A + B); X := Y; end My_Procedure; I get a semantic error (112) at the 'use type'. "A use type clause may not appear here. They are only permitted as part of a context clause or directly following an embedded package specification." (although, of course, a use type clause never needs to reference a type in the same package). > While if I have something like > > procedure My_Procedure > is > use type My_Type; > begin > ... bla-bla-bla ... > end My_Procedure; > > Then the spark syntax checker complains Syntax Error reserved "IS" cannot > be followed by "USE" here. I do get that error (which is to be expected since a 'use type' clause must follow a semi-colon). > Is SPARK missing something or is there a rational ? Not sure, unless you can post your complete SPARKable code? Cheers, Phil
From: Rod Chapman on 25 May 2010 03:29 >On May 25, 12:01 am, Phil Thornley <phil.jpthorn...(a)googlemail.com> wrote: Phil is basically correct. "use type" is only permitted in the language definition in two places: 1) As a context clause 2) Directly following an embedded package specification. BUT... 1) is fully implemented. 2) is NOT implemented by any version of the Examiner. This is documented (somewhat briefly) in section 11.1.1 of the toolset release note, and page 402 of the book. - Rod
From: Yannick Duchêne (Hibou57) on 25 May 2010 16:05 Le Tue, 25 May 2010 01:01:08 +0200, Phil Thornley <phil.jpthornley(a)googlemail.com> a écrit: > On 24 May, 19:41, Yannick Duchêne (Hibou57) <yannick_duch...(a)yahoo.fr> > wrote: >> Hi, >> >> I meet a strange behavior with the SPARK syntax checker (via the >> examiner). > > I can't get the behaviour that you are reporting (I'm still on GPL > version 8.1.1) I'm using SPARK 8.1.1 too (I'm not working for a company). > - can you post a complete SPARKable example? Sure, here are two: package body Dummies is procedure Dummy is use type Natural; Entity : Natural; begin null; end Dummy; end Dummies; This latter fails syntax check pass with the message âSyntax Error reserved word "IS" cannot be followed by reserved word "USE" here.â package body Dummies is procedure Dummy is Entity : Natural; use type Natural; begin null; end Dummy; end Dummies; This latter one pass syntax check without any error message (just two obvious warnings). The only difference, is the place where the âuse typeâ clause comes. If it comes first, an error message is raised, if it comes after any declaration (type or entity), that's OK. > This definitely should not be OK, 'use type' clauses should (normally) > only appear as part of a context clause. Eh, I'm dreaming, I have the result I am reporting. > With this code in a package body: > > type A_Type is range 1 .. 10; > > procedure My_Procedure(A : in A_Type; > B : in A_Type; > X : out Integer) > --# derives X from A, B; > is > Y : Integer; > use type A_Type; > begin > Y := Integer(A + B); > X := Y; > end My_Procedure; I was doing a syntax check only (I feel it is important to state this, as you come with an example using Derives clauses). I am preparing a set of packages to be later checked with SPARK. As a first step, I have to modify some little stuff to ensure it is valid SPARK syntax (like adding explicit type indication in âfor Index in 1 ... Nâ which have to be turned into âfor Index in Index_Type range 1 .. Nâ). This is doing so, I've meet this strange thing. -- There is even better than a pragma Assert: a SPARK --# check.
From: Yannick Duchêne (Hibou57) on 25 May 2010 16:16 Le Tue, 25 May 2010 09:29:43 +0200, Rod Chapman <roderick.chapman(a)googlemail.com> a écrit: >> On May 25, 12:01 am, Phil Thornley <phil.jpthorn...(a)googlemail.com> >> wrote: > > Phil is basically correct. > > "use type" is only permitted in the language definition in two places: > > 1) As a context clause > > 2) Directly following an embedded package specification. > > BUT... > > 1) is fully implemented. > > 2) is NOT implemented by any version of the Examiner. > > This is documented (somewhat briefly) in section 11.1.1 of > the toolset release note, and page 402 of the book. > - Rod Unfortunately, I've understood the documentation is somewhat incorrect or at least is missing some stuffs, so I'm not always referring to it. As an example, the SPARK 95 reference states that renames clause can be use to drop parent part of package path only and the package have to be renamed using its original name exactly ; so, Parent.Child should only be renamed as Child to be able to refer to it without having to write the âParent.â every where. But I could rename some package using other names. The same with procedures renaming. The same with generics. The SPARK reference say the only generic instantiation allowed is instantiation of Unchecked_Conversion. However, I have some generic packages instantiation, and the syntax checker do not complain at all about it. Well, may be it will fail later at the semantic analysis, I hope not, or else I will have to drop SPARK... I believe it will be OK, as I saw some words somewhere stating SPARK now support generic. Time to say I've also encountered strange things with generic instantiation. I can instantiate a generic package only if the package name has no prefix and trying to instantiate something like âis new Parent.Child (Formal_Parameter => ...)â fails, and âis new Child (Formal_Parameter => ...)â is accepted. -- There is even better than a pragma Assert: a SPARK --# check.
|
Next
|
Last
Pages: 1 2 Prev: Ada-Belgium Spring 2010 Event, registration deadline approaching Next: Emacs and long file names |