Expose ACSL annotations through host language pragmas

ID0002370: This issue was created automatically from Mantis Issue 2370. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0002370	Frama-C	Kernel > ACSL implementation	public	2018-03-08	2018-03-08

Reporter	pini	Assigned To	virgile	Resolution	open
Priority	normal	Severity	feature	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C 16-Sulfur	Target Version	-	Fixed in Version	-

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.