Statically reject programs that jump over VLA declaration.

ID0001712: This issue was created automatically from Mantis Issue 1712. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0001712	Frama-C	Kernel	public	2014-03-24	2014-03-24

Reporter	pascal	Assigned To	virgile	Resolution	open
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	-	Target Version	-	Fixed in Version	-

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; } }