Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002370Frama-CKernel > ACSL implementationpublic2018-03-08 20:252018-03-08 20:25
Assigned Tovirgile 
PlatformOSOS Version
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

- Relationships

-  Notes
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

Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker