2021-02-24 18:51 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000852Frama-CKernelpublic2013-01-25 22:29
ReporterJochen 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in Version 
Summary0000852: non-constant size of 2-dim array causes error in recursive procedure
DescriptionCalling "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.
TagsNo tags attached.
Attached Files
  • c file icon ftest.c (33 bytes) 2011-06-01 17:31 -
    void main(int *a,int c[*a]) {}
    
    
    c file icon ftest.c (33 bytes) 2011-06-01 17:31 +

-Relationships
related to 0000856closedyakobowski non-constant size of 2-dim array leads to crash (some similarities to issue 0000852
+Relationships

-Notes

~0001947

pascal (reporter)

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.

~0001948

Jochen (reporter)

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)

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)

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