Re: SPARK syntax and “use type” : lack of feature ?

[Phil Thornley <phil.jpthornley@googlemail.com>]

On 24 May, 19:41, Yannick Duchêne (Hibou57) <yannick_duch...@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