rems-project / cerberus

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

[CN] Retire the ability to break up specifications across magic comments #503

Open dc-mak opened 1 month ago

dc-mak commented 1 month ago

This is an artefact of prior versions and should probably be disallowed (verbose, less to explain, less to document, cleaner code...)

https://github.com/rems-project/cerberus/blob/f83846aea10cb0b62d16f506448773f6d860b684/tests/cn/swap.c#L3-L8

septract commented 1 month ago

I'm in favor, but I think many of the examples in the example-archive don't conform to this standard. So some upgrade would be needed.

(edit: since I figured it out, this is a regex to find such cases using VS Code search: @\*/[\s\n]*/\*@\s*)