0002370: Expose ACSL annotations through host language pragmas

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0002370

Frama-C

Kernel > ACSL implementation

public

2018-03-08 20:25

Reporter

pini

Assigned To

virgile

Priority

normal

Severity

feature

Reproducibility

always

Status

assigned

Resolution

open

Platform

OS Version

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.

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

Relationships

Notes
There are no notes attached to this issue.