Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000852Frama-CKernelpublic2011-06-01 17:312013-01-25 22:29
Assigned Tovirgile 
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 #852) 

-  Notes
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.
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).

- 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 - 2020 MantisBT Team
Powered by Mantis Bugtracker