Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001645Frama-CKernelpublic2014-02-13 19:212014-03-24 18:10
Reporterpascal 
Assigned Tovirgile 
PrioritylowSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Fluorine-20130601 
Target VersionFixed in Version 
Summary0001645: Initializer of static variable refers to size of type of local variable
DescriptionCONTEXT:
This issue does not originate from an industrial application. It is reported for the lulz.

DESCRIPTION:
The program below is accepted by gcc and clang, and rejected by Frama-C. It seems that the compilers are right to accept it.

~ $ cat t.c

unsigned f(void) {
 int a;
 static unsigned s = sizeof(a);
 return s;
}

~ $ clang -std=c99 -pedantic -Wall -c t.c
~ $ frama-c t.c
[kernel] preprocessing with "gcc -C -E -I. t.c"
t.c:4:[kernel] user error: Forbidden access to local variable a in static initializer
[kernel] user error: skipping file "t.c" that has errors.
[kernel] Frama-C aborted: invalid user input.
~ $
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2014-02-13 19:21 pascal New Issue
2014-03-24 18:10 signoles Assigned To => virgile
2014-03-24 18:10 signoles Status new => assigned


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker