search

rems-project / cerberus

Cerberus C semantics
https://www.cl.cam.ac.uk/~pes20/cerberus/
Other
49 stars 25 forks source link

[CN] Introduce a different special syntax for CN specs #263

Closed podhrmic closed 3 months ago

podhrmic commented 4 months ago

Currently CN and Frama-C specs collide, as they both use /@ for their special syntax. As a result, it is not possible to have CN and Frama-C specs in the same codebase at the same time. Since we cannot easily change the Frama-C parser, I suggest using different CN specs syntax, e.g. , //@ vs. /*@ vs. /**@ and pragmas like //@ safemath - the inspiration can be drawn from JML.

This should be an easy fix, as you are replacing one token with another, and you can sed edit the existing examples/codebase.

septract commented 4 months ago

If changing the existing magic comment syntax in one big bang is too painful, we could just offer an alternative CN-specific syntax. Then we would just use the alternative in VERSE so that we can mix Frama-C and CN specifications.

Re the proposals above, whatever we choose should also serve as a delimiter for multi-line comments for C. So /**@ is okay, but something like //@ is not going to work.

A couple of alternatives that don't look too horrible: /*#, /*~

PeterSewell commented 4 months ago

It's surely not hard to do something if there's need, but it seems a bit messy - why/when do we want to have both at once, rather than versions of examples using one or the other?

On Wed, 22 May 2024 at 10:14, Mike Dodds @.***> wrote:

If changing the existing magic comment syntax in one big bang is too painful, we could just offer an alternative CN-specific syntax. Then we would just use the alternative in VERSE so that we can mix Frama-C and CN specifications.

Re the proposals above, whatever we choose should also serve as a delimiter for multi-line comments for C. So /**@ is okay, but something like //@ is not going to work.

A couple of alternatives that don't look too horrible: /#, /~

— Reply to this email directly, view it on GitHub https://github.com/rems-project/cerberus/issues/263#issuecomment-2124272832, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABFMZZXIG2I3CCJG7YZGWYDZDROVVAVCNFSM6AAAAABICDBJX2VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCMRUGI3TEOBTGI . You are receiving this because you are subscribed to this thread.Message ID: @.***>

podhrmic commented 4 months ago

We came across this when porting the Mission Protection System on OpenSUT from the original HARDENS project. The original code has Frama-C specs, and the ideal workflow would be to preserve the Frama-C proofs, while adding CN proofs. I expect running into this issue again as we port other OpenSUT components as they have existing Frama-C specs as well.

thatplguy commented 4 months ago

My vote would be to support two comment syntaxes for CN, the current one plus a second that deconflicts Frama-C. This avoids changing all the examples and the tutorial for what I imagine will be an uncommon use case, while still supporting Frama-C specs in the OpenSUT. Joe mentioned that JML supports multiple special comment syntaxes partly for this reason.

yav commented 3 months ago

The /** is used for doc comments by doxygen, so it'd be good to avoid clashing with that also.

dc-mak commented 3 months ago

Fixed by https://github.com/rems-project/cerberus/commit/60d013553e414522e55994b8f6cf55fa746f47bf