View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|
0002370 | Frama-C | Kernel > ACSL implementation | public | 2018-03-08 20:25 | 2018-03-08 20:25 | ||||||||
Reporter | pini | ||||||||||||
Assigned To | virgile | ||||||||||||
Priority | normal | Severity | feature | Reproducibility | always | ||||||||
Status | assigned | Resolution | open | ||||||||||
Product Version | Frama-C 16-Sulfur | ||||||||||||
Target Version | Fixed in Version | ||||||||||||
Summary | 0002370: Expose ACSL annotations through host language pragmas | ||||||||||||
Description | Instead of using comments, that are non-specific constructs and may be mixed with non-ACSL comments from a parser or renderer point of view, would it be possible to use the C standard pragma construct? Instead of e.g. /*@ requires R: \valid(ptr); @*/ this would give either (pragma directive): #pragma ACSL requires R: \valid(ptr); or (pragma operator): _Pragma("ACSL requires R: \valid(ptr);") This would help specify ACSL annotations in a specific language construct and as such expose them properly to outside programs (IDE, editors, documentation generators, etc.) This could of course co-exist along with the current comment form. | ||||||||||||
Tags | No tags attached. | ||||||||||||
Attached Files |
|