| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 0000852 | Frama-C | Kernel | public | 2011-06-01 17:31 | 2013-01-25 22:29 | ||||||||
| Reporter | Jochen | ||||||||||||
| Assigned To | virgile | ||||||||||||
| Priority | normal | Severity | minor | Reproducibility | always | ||||||||
| Status | assigned | Resolution | open | ||||||||||
| Product Version | Frama-C Carbon-20110201 | ||||||||||||
| Target Version | Fixed in Version | ||||||||||||
| Summary | 0000852: non-constant size of 2-dim array causes error in recursive procedure | ||||||||||||
| Description | 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. | ||||||||||||
| Tags | No tags attached. | ||||||||||||
| Attached Files |
| ||||||||||||
 Relationships |
||||||
|
||||||
 Relationships |
| Notes |
|
|
pascal (reporter) 2011-06-01 17:53 Last edited: 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. |
|
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> |
|
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. |
|
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). |
| Notes |
| 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 | Assigned To | pascal => virgile |
| 2011-06-01 17:50 | pascal | Category | Plug-in > value analysis => Kernel |
| 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 | |
| Issue History |