Annotations outside of source files

[vprevosto]

Some development processes require that source code stays unmodified during V&V. This causes an issue when one wants to add annotation to prove a property. Possible solutions for implementations should be discussed in an appendix of the file.

• global annotations and function contracts can be put in an additional .h file that is not part of the original sources
• statement annotations can be given as .patch files
• or with a specific mechanism to attach them to a given statement with a DSL for statement selection.

[pbaudin]

Notice that the ACSL importer plug-in (CEA proprietary) of Frama-C already implements such a mechanism allowing the import of external files containing the ACSL specifications. A language extension, built over ACSL itself, as been defined for that.