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
Reporterpini 
Assigned Tovirgile 
PrioritynormalSeverityfeatureReproducibilityalways
StatusassignedResolutionopen 
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 - 2019 MantisBT Team
Powered by Mantis Bugtracker