Expose ACSL annotations through host language pragmas
ID0002370: This issue was created automatically from Mantis Issue 2370. Further discussion may take place here.
|ID0002370||Frama-C||Kernel > ACSL implementation||public||2018-03-08||2018-03-08|
|Product Version||Frama-C 16-Sulfur||Target Version||-||Fixed in Version||-|
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.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information