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 
DOC++ tool uses two keywords, //@{ and //@} which interfere with Frama-C. 
Of course and as expected, when Frama-C encounters one, it just stops with 
a syntax error.

A presentation of DOC++ can be found at and a 
very short (less than a page and showing the potential problem) quickstart 
can be found at . 

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 reserved 
for proof-related program annotations? Does anyone have other examples of 
such collisions?

Jean-Baptiste Jeannin
" This e-mail and any attached documents may contain confidential or proprietary information. If you are not the intended recipient, please advise the sender immediately and delete this e-mail and all attached documents from your computer system. Any unauthorised disclosure, distribution or copying hereof is prohibited."

 " Ce courriel et les documents qui y sont attaches peuvent contenir des informations confidentielles. Si vous n'etes  pas le destinataire escompte, merci d'en informer l'expediteur immediatement et de detruire ce courriel  ainsi que tous les documents attaches de votre systeme informatique. Toute divulgation, distribution ou copie du present courriel et des documents attaches sans autorisation prealable de son emetteur est interdite."
-------------- next part --------------
An HTML attachment was scrubbed...