--- layout: fc_discuss_archives title: Message 113 from Frama-C-discuss on October 2008 ---
[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