Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Collisions using //@ or /*@

>
>> Some JavaDoc-like documentation tools can badly interfere with  
>> Frama-C by
>> also requiring special comments beginning by /*@ or //@. For  
>> example, the
>> Do you have any idea of how to go around this problem? Are the /*@  
>> and //@
>> syntaxes, which were already used by JML, supposed to somehow be
>
> In the current version of Frama-C (and in the forthcoming release),  
> the
> only way to overcome this issue is to disable annotation processing
> entirely (with the -no-annot option). The '@' sign was indeed chosen  
> to
> introduce ACSL annotation because it was already used by JML (while
> javadoc and doxygen use '*' for structured documentation).

However, I should add that the expected character for ACSL annotations  
is
not hardwired anywhere in Frama-C.
It will be relatively easy to introduce a command-line
option to change this character for compatibility with other  
annotation tools
in the future.

Pascal