Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000713Frama-CKernel > ACSL implementationpublic2011-02-10 12:272011-02-10 12:27
Reporterboris 
Assigned Tovirgile 
PrioritynormalSeverityfeatureReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Carbon-20101202-beta2 
Target VersionFixed in Version 
Summary0000713: Any number of ";" should be allowed in specifications
DescriptionThe specification below produces a syntax error. As in C, any number of ";" should be allowed in specifications.

Additional Information#define v(this) requires \valid(this);

/*@ v(this);
    v(&this->a);
*/
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2011-02-10 12:27 boris New Issue
2011-02-10 12:27 boris Status new => assigned
2011-02-10 12:27 boris Assigned To => virgile


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker