search

acsl-language / acsl

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

@ symbols #34

Open davidcok opened 6 years ago

davidcok commented 6 years ago

The introduction says that @ symbols in an annotation are equivalent to blanks. But the section on ghost code says that @ symbols at the beginning of lines and end of the comment are blanks, which does not include all @ symbols.

Which is it to be?

vprevosto commented 6 years ago

The former: all @ symbols in an ACSL annotations are considered as blanks.

jensgerlach commented 6 years ago

This might no be the best place to mention this but I this issue reminds me of an idea Loïc told me about: If x is a variable (or lvalue?) and L a label, then instead of \at(x, L) one is allowed to write x@L.

I think this looks neat!