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