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=ham autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,aa0ebfe6afda2b3
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,UTF8
Path: 
 g2news2.google.com!news1.google.com!goblin1!goblin2!goblin.stu.neva.ru!aioe.org!not-for-mail
From: =?utf-8?Q?Yannick_Duch=C3=AAne_=28Hibou57?=
 =?utf-8?Q?=29?=
 <yannick_duchene@yahoo.fr>
Newsgroups: comp.lang.ada
Subject: Re:
 =?utf-8?B?U1BBUksgc3ludGF4IGFuZCDigJx1c2UgdHlwZeKAnSA6IGxhY2sgb2YgZmU=?=
 =?utf-8?B?YXR1cmUgPw==?=
Date: Tue, 25 May 2010 22:05:12 +0200
Organization: Ada At Home
Message-ID: <op.vc912yr1ule2fv@garhos>
References: <op.vc73ixt2ule2fv@garhos>
 <17c936fc-66ce-4bb9-ba5a-069d9ed5a2fe@l6g2000vbo.googlegroups.com>
NNTP-Posting-Host: lwoedXCBwVNAtSGnEUHIWA.user.speranza.aioe.org
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed; delsp=yes
Content-Transfer-Encoding: Quoted-Printable
X-Complaints-To: abuse@aioe.org
X-Notice: Filtered by postfilter v. 0.8.2
User-Agent: Opera Mail/10.53 (Win32)
Xref: g2news2.google.com comp.lang.ada:11986
Date: 2010-05-25T22:05:12+02:00
List-Id: <comp.lang.ada>

Le Tue, 25 May 2010 01:01:08 +0200, Phil Thornley  =

<phil.jpthornley@googlemail.com> a =C3=A9crit:

> On 24 May, 19:41, Yannick Duch=C3=AAne (Hibou57) <yannick_duch...@yaho=
o.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 =E2=80=9CSyntax Err=
or   =

reserved word "IS" cannot be followed by reserved word "USE" here.=E2=80=
=9D

    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 =E2=80=9Cuse type=E2=80=9D c=
lause comes. If it  =

comes first, an error message is raised, if it comes after any declarati=
on  =

(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 :=3D Integer(A + B);
>        X :=3D Y;
>     end My_Procedure;
I was doing a syntax check only (I feel it is important to state this, a=
s  =

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 SPA=
RK  =

syntax (like adding explicit type indication in =E2=80=9Cfor Index in 1 =
.. N=E2=80=9D  =

which have to be turned into =E2=80=9Cfor Index in Index_Type range 1 ..=
 N=E2=80=9D).

This is doing so, I've meet this strange thing.

-- =

There is even better than a pragma Assert: a SPARK --# check.