Frama-C Bug Tracking System - Frama-C
View Issue Details
0000713Frama-CKernel > ACSL implementationpublic2011-02-10 12:272011-02-10 12:27
boris 
virgile 
normalfeaturealways
assignedopen 
Frama-C Carbon-20101202-beta2 
 
0000713: Any number of ";" should be allowed in specifications
The specification below produces a syntax error. As in C, any number of ";" should be allowed in specifications.
#define v(this) requires \valid(this); /*@ v(this); v(&this->a); */
No tags attached.
Issue History
2011-02-10 12:27borisNew Issue
2011-02-10 12:27borisStatusnew => assigned
2011-02-10 12:27borisAssigned To => virgile

There are no notes attached to this issue.