Re: SPARK reserved and predefined words : alternative choices

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

Le Thu, 20 May 2010 11:01:30 +0200, Rod Chapman  
<roderick.chapman@googlemail.com> a écrit:
> You can, of course, use the -fdl=XXXX switch
> to de-conflict the name-space if you like. In that case,
> the predefined FDL identifiers are usable.  See the Examiner
> User Manual for details.

There is something funny with this option. The documentation says it is  
"-fd" and also refer to it as "-fdl".

    -fd=string:

    This switch controls the Examiner’s treatment
    of FDL reserved words (see section 5.3). The
    option -fd=reject, or any abbreviation of
    ‘reject’, rejects all FDL reserved words as being
    syntactically unacceptable. This is the default.
    The option -fd=accept, or any abbreviation
    of ‘accept’, suppresses the rejection of FDL
    reserved words, but also prevents the
    generation of any proof files. Any string other
    than ‘reject’ or ‘accept’ (or their abbreviations)
    causes recognised FDL reserved words to be
    mangled on output by placing the string before
    the identifier, separated by a double underbar.
    As an example, -fdl=praxis would cause
    the identifier start to be output as
    praxis__start. Previously this was a binary
    option (-fdl_identifiers and -
    nofdl_identifiers) and this form is still
    supported, but deprecated.

Mangling is what is needed, indeed. If this work, I will use it as a  
default option everywhere. Something like “-fdl=arg” or “-fdl=app” should  
be enough. Sources relying on this should add a note about in a README or  
some of the like.

There was an option which deals with only one specific keywords, and I  
though this was the only one.

Thanks Rod, that's the tip of the day.

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