Frama-C Bug Tracking System - Frama-C
View Issue Details
0000852Frama-CKernelpublic2011-06-01 17:312013-01-25 22:29
Jochen 
virgile 
normalminoralways
assignedopen 
Frama-C Carbon-20110201 
 
0000852: non-constant size of 2-dim array causes error in recursive procedure
Calling "frama-c -val ftest.c" for the attached program results in a kernel error message "Invalid length in array type". The error vanishes if either - the recursive call in the body is removed, - the 2-dimensional array (b[1][a]) is made a one-dimensional one (b[a]), - or the variable size (b[1][a]) is made constant (b[1][9]). Since I cannot imagine why just the combination (recursion + two dimensions + variable size) shall be an error, I guess there is a bug here. Moreover, even the Jessie plug-in reports only warnings on ftest.c.
No tags attached.
related to 0000856closed yakobowski non-constant size of 2-dim array leads to crash (some similarities to issue #852) 
c ftest.c (33) 2011-06-01 17:31
https://bts.frama-c.com/file_download.php?file_id=227&type=bug
Issue History
2011-06-01 17:31JochenNew Issue
2011-06-01 17:31JochenStatusnew => assigned
2011-06-01 17:31JochenAssigned To => pascal
2011-06-01 17:31JochenFile Added: ftest.c
2011-06-01 17:50pascalNote Added: 0001946
2011-06-01 17:50pascalAssigned Topascal => virgile
2011-06-01 17:50pascalCategoryPlug-in > value analysis => Kernel
2011-06-01 17:52pascalNote Deleted: 0001946
2011-06-01 17:53pascalNote Added: 0001947
2011-06-01 17:59pascalNote Edited: 0001947
2011-06-01 18:11JochenNote Added: 0001948
2011-06-01 18:46pascalNote Added: 0001949
2011-06-07 13:22pascalRelationship addedrelated to 0000856
2013-01-25 22:29yakobowskiNote Added: 0003675

Notes
(0001947)
pascal   
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   
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   
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   
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).