Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002147Frama-CKernel > ACSL implementationpublic2015-07-16 19:452015-07-16 19:45
Reporterdcok@grammatech.com 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Sodium 
Target VersionFixed in Version 
Summary0002147: Frama-C problem with macro substitution in annotations
DescriptionThis piece of code should parse with frama-c, but does not: #define MACRO 3 void m() { char buf[MACRO+1]; //@ assert \valid(buf+(0..MACRO)); } Upon execution, frama-c gives back "[kernel] user error: unbound logic variable MACRO in annotation.". This piece of code, however, executes as it should: #define MACRO 3 void m() { char buf[MACRO+1]; //@ assert \valid(buf+(0.. MACRO)); } This code is also okay: #define MACRO 3 void m() { char buf[MACRO+1]; //@ assert \valid(buf+(0..(MACRO))); } It seems that frama-c refuses to substitute defines directly after a .. operator.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2015-07-16 19:45 dcok@grammatech.com New Issue
2015-07-16 19:45 dcok@grammatech.com Status new => assigned
2015-07-16 19:45 dcok@grammatech.com Assigned To => virgile


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker