0002147: Frama-C problem with macro substitution in annotations

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0002147

Frama-C

Kernel > ACSL implementation

public

2015-07-16 19:45

Reporter

dcok@grammatech.com

Assigned To

virgile

Priority

normal

Severity

minor

Reproducibility

always

Status

assigned

Resolution

open

Platform

OS Version

Product Version

Frama-C Sodium

Target Version

Fixed in Version

Summary

0002147: Frama-C problem with macro substitution in annotations

Description

This 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.

Tags

No 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