2021-03-05 02:20 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002370Frama-CKernel > ACSL implementationpublic2018-03-08 20:25
Assigned Tovirgile 
Product VersionFrama-C 16-Sulfur 
Target VersionFixed in Version 
Summary0002370: Expose ACSL annotations through host language pragmas
DescriptionInstead 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.

TagsNo tags attached.
Attached Files


There are no notes attached to this issue.

-Issue History
Date Modified Username Field Change
2018-03-08 20:25 pini New Issue
2018-03-08 20:25 pini Status new => assigned
2018-03-08 20:25 pini Assigned To => virgile
+Issue History