search

acsl-language / acsl

Sources for the ANSI/ISO C Specification Language manual
Other
49 stars 8 forks source link

Ghost code and annotation #3

Closed vprevosto closed 4 years ago

vprevosto commented 7 years ago

Is the usage of /@ @/ to delimit multi-line annotations in ghost code the best way to handle, or should we stick to /*@ ... */ event if that means nested comments for standard C compiler?

davidcok commented 6 years ago

Since ghost code is already in an annotation comment, does the specification for the ghost code need to be in an embedded comment? Or would omitting such delimiters make problems for the parser?

vprevosto commented 6 years ago

Omitting the delimiters would indeed complicate things for the parser, as ACSL and C (ghost or not) syntaxes are quite different. Having delimiters makes it easy to know when to switch between the two.

In addition, the development version of Frama-C recently gained support for /@ @/ in ghost code, making the issue rather moot.