You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
CN delimits its specifications with a "magic comment" syntax, by default /*@ ... @*/. The VSCode plugin currently assumes that all CN specifications are written using this syntax. Because this syntax clashes with Frama-C's contract syntax, however, CN implemented an optional alternative syntax, /*$ ... $*/ (see rems-project/cerberus#263). The VSCode plugin should allow users to choose which syntax to use.
Note that choosing one comment syntax should make the plugin ignore comments written with the other syntax. The motivation here is to allow running CN and Frama-C plugins concurrently on a file containing both CN and Frama-C annotations. Users in this situation (assuming they've selected the $ syntax for CN) ought to see Frama-C-related workflows appear only for @-delimited blocks and CN-related integrations appear only for $-delimited blocks.
A basic implementation of this feature would set a user's choice of comment syntax globally. In the future, we may want an implementation to set this choice locally, to better support users who may have some projects where CN annotations are written with @, and others where they're written with $. The precise definition of locally is up for debate. Should it be per-file, per-directory, per-repository? Can the plugin try to automatically recognize which syntax is used?
CN delimits its specifications with a "magic comment" syntax, by default
/*@ ... @*/
. The VSCode plugin currently assumes that all CN specifications are written using this syntax. Because this syntax clashes with Frama-C's contract syntax, however, CN implemented an optional alternative syntax,/*$ ... $*/
(see rems-project/cerberus#263). The VSCode plugin should allow users to choose which syntax to use.Note that choosing one comment syntax should make the plugin ignore comments written with the other syntax. The motivation here is to allow running CN and Frama-C plugins concurrently on a file containing both CN and Frama-C annotations. Users in this situation (assuming they've selected the
$
syntax for CN) ought to see Frama-C-related workflows appear only for@
-delimited blocks and CN-related integrations appear only for$
-delimited blocks.A basic implementation of this feature would set a user's choice of comment syntax globally. In the future, we may want an implementation to set this choice locally, to better support users who may have some projects where CN annotations are written with
@
, and others where they're written with$
. The precise definition of locally is up for debate. Should it be per-file, per-directory, per-repository? Can the plugin try to automatically recognize which syntax is used?cc @septract
The text was updated successfully, but these errors were encountered: