Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000852Frama-CKernelpublic2011-06-01 17:312013-01-25 22:29
ReporterJochen 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
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 Filesc file icon ftest.c [^] (33 bytes) 2011-06-01 17:31 [Show Content]

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

-  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

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker