Re: SPARK POGS: List the rules used by the Simplifier

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

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

> So this report the kind of things which is otherwise split through  
> 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