0000852: non-constant size of 2-dim array causes error in recursive procedure

Notes
(0001947) pascal (reporter) 2011-06-01 17:53 edited on: 2011-06-01 17:59	Jochen, could you provide the exact file and command-line that cause what you consider to be wrong behavior, and paste the output that you get as well? I have: ~/ppc $ cat ftest.c void main(int a,int c[a]) {} ~/ppc $ /usr/local/Frama-C_Carbon/bin/frama-c -val ftest.c [kernel] preprocessing with "gcc -C -E -I. ftest.c" ftest.c:2:[kernel] warning: MEMOF in constant ftest.c:2:[kernel] warning: Cannot represent the length of array as an attribute [value] Analyzing a complete application starting at main [value] Computing initial state [value] Initial state computed [value] Values of globals at initialization [value] Recording results for main [value] done for function main [value] ====== VALUES COMPUTED ====== [value] Values for function main: ~/ppc $ And I do not see what is bothering you.

(0001948) Jochen (reporter) 2011-06-01 18:11	I just realized that somehow I attached the wrong file ftest.c - please apologize. Here is what I get with the right one: sh> cat ftest.c void ftest(int a,int b[1][a]) { ftest(a,b); } sh> frama-c -val ftest.c [kernel] warning: cannot load 2 plug-ins (incompatible with Carbon-20110201). Ltl_to_acsl; Wp [kernel] preprocessing with "gcc -C -E -I. ftest.c" ftest.c:4:[kernel] user error: Invalid length in array type: a [kernel] user error: skipping file "ftest.c" that has errors. [kernel] Frama-C aborted because of invalid user input. sh>

(0001949) pascal (reporter) 2011-06-01 18:46	This is indeed a kernel error, -val is not necessary to obtain the error: ~ $ ~/ppc/bin/toplevel.opt ftest.c [kernel] preprocessing with "gcc -C -E -I. t.c" [kernel] user error: Invalid length in array type: a [kernel] user error: skipping file "t.c" that has errors. [kernel] error occurring when exiting Frama-C: stopping exit procedure. Frama-C aborted because of invalid user input.

(0003675) yakobowski (manager) 2013-01-25 22:29	Oxygen accepts this program, but -check fails. Declaring a two-dimensional non-constant array with 'int b[10][a];' results in an error (but not a crash).

Issue History
Date Modified	Username	Field	Change
2011-06-01 17:31	Jochen	New Issue
2011-06-01 17:31	Jochen	Status	new => assigned
2011-06-01 17:31	Jochen	Assigned To	=> pascal
2011-06-01 17:31	Jochen	File Added: ftest.c
2011-06-01 17:50	pascal	Note Added: 0001946
2011-06-01 17:50	pascal	Assigned To	pascal => virgile
2011-06-01 17:50	pascal	Category	Plug-in > value analysis => Kernel
2011-06-01 17:52	pascal	Note Deleted: 0001946
2011-06-01 17:53	pascal	Note Added: 0001947
2011-06-01 17:59	pascal	Note Edited: 0001947
2011-06-01 18:11	Jochen	Note Added: 0001948
2011-06-01 18:46	pascal	Note Added: 0001949
2011-06-07 13:22	pascal	Relationship added	related to 0000856
2013-01-25 22:29	yakobowski	Note Added: 0003675