0001712: Statically reject programs that jump over VLA declaration.

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0001712

Frama-C

Kernel

public

2014-03-24 16:28

2014-03-24 18:10

Reporter

pascal

Assigned To

virgile

Priority

normal

Severity

minor

Reproducibility

always

Status

assigned

Resolution

open

Platform

OS Version

Product Version

Target Version

Fixed in Version

Summary

0001712: Statically reject programs that jump over VLA declaration.

Description

The following program contains UB (jumping over the declaration of t):

int main(int c, char **v){
  goto label;
  {
    char t[c];
    f(t);
  label:
    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;
    {
      /*sequence*/
      __lengthoft = (unsigned int)c;
      t = (char *)__builtin_alloca(sizeof(*t) * __lengthoft);
    }
    f(t);
    label: ;
    __retres = (int)*(t + 0);
    return __retres;
  }
}

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

Relationships

Notes
There are no notes attached to this issue.