2021-01-15 18:17 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001712Frama-CKernelpublic2014-03-24 18:10
Assigned Tovirgile 
Product Version 
Target VersionFixed in Version 
Summary0001712: Statically reject programs that jump over VLA declaration.
DescriptionThe following program contains UB (jumping over the declaration of t):

int main(int c, char **v){
  goto label;
    char t[c];
    return t[0];

It would be nice it was rejected by the front-end.

This is not absolutely necessary, in the sense that Frama-C has historically focused on bugs not found by compilers and neglected those that could be found reliably by compilers (both GCC and Clang reject the program). But it would be nice.
Steps To Reproduce[kernel] preprocessing with "gcc -C -E -I. t.c"
t.c:4:[kernel] warning: Variable-sized local variable t
t.c:5:[kernel] warning: Calling undeclared function f. Old style K&R code?
/* Generated by Frama-C */
/* compiler builtin:
   void *__builtin_alloca(unsigned int); */
extern int ( /* missing proto */ f)(char *x_0);

int main(int c, char **v)
  int __retres;
  goto label;
    char *t;
    unsigned int __lengthoft;
      __lengthoft = (unsigned int)c;
      t = (char *)__builtin_alloca(sizeof(*t) * __lengthoft);
    label: ;
    __retres = (int)*(t + 0);
    return __retres;
TagsNo tags attached.
Attached Files


There are no notes attached to this issue.

-Issue History
Date Modified Username Field Change
2014-03-24 16:28 pascal New Issue
2014-03-24 18:10 signoles Assigned To => virgile
2014-03-24 18:10 signoles Status new => assigned
+Issue History