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