2021-01-21 05:15 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001645Frama-CKernelpublic2014-03-24 18:10
Assigned Tovirgile 
Product VersionFrama-C Fluorine-20130601 
Target VersionFixed in Version 
Summary0001645: Initializer of static variable refers to size of type of local variable
This issue does not originate from an industrial application. It is reported for the lulz.

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


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
+Issue History