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=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD,
	FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: 103376,3f4112f9d4cec374
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII
Path: 
 g2news1.google.com!postnews.google.com!i31g2000yqm.googlegroups.com!not-for-mail
From: Phil Thornley <phil.jpthornley@gmail.com>
Newsgroups: comp.lang.ada
Subject: Re: SPARK POGS: List the rules used by the Simplifier
Date: Fri, 13 Aug 2010 12:04:00 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <25335b0c-f1d6-4816-be30-a2c8c71018e9@i31g2000yqm.googlegroups.com>
References: <0885ddcf-4d87-4cb5-a7ff-53d4397e0c8a@j8g2000yqd.googlegroups.com>
 <op.vhd09cwcxmjfy8@garhos>
NNTP-Posting-Host: 80.177.171.182
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
X-Trace: posting.google.com 1281726240 10058 127.0.0.1 (13 Aug 2010 19:04:00
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Fri, 13 Aug 2010 19:04:00 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: i31g2000yqm.googlegroups.com; posting-host=80.177.171.182;
 posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 8.0; Windows NT 6.1; WOW64;
 Trident/4.0; SLCC2; .NET CLR 2.0.50727; .NET CLR 3.5.30729; .NET CLR
 3.0.30729; Media Center PC 6.0; .NET4.0C),gzip(gfe)
Xref: g2news1.google.com comp.lang.ada:13233
Date: 2010-08-13T12:04:00-07:00
List-Id: <comp.lang.ada>

On 13 Aug, 18:52, Yannick Duch=EAne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:

> So this report the kind of things which is otherwise split through =A0
> multiple *.rls files ?

No - *.rls files are produced by the Examiner, so it doesn't really
matter which of the rules in these files are used (in fact most of
them are not used).

These summaries are of the user rules - in *.rlu files - which are
hand coded and so have to be reviewed and maintained as the code
develops.  It's useful to be able to keep these rules to a minimum to
keep the maintenance load down.

(And, for example, one of the changes with SPARK 2010 will remove the
need for user rules for function return annotations, so these
summaries will help to identify which those rules are.)

In fact this information is already in the POGS summary - but it is
given for each operation, ahead of the table showing each VC in the
operation, and the way that it is presented makes it tedious to
identify which rules have/have not been used - particularly for
'package' rule files that might be used by a number of different
operations.

Cheers,

Phil