Actions
Bug #4789
openMissing extern declarations for the arrays
Start date:
03/25/2014
Due date:
% Done:
0%
Estimated time:
Detected in build:
svn
Platform:
Published in build:
Description
For the driver
linux-3.12-rc1.tar.xz 32_7a drivers/media/v4l2-core/videodev.ko ldv_main0_sequence_infinite_withcheck_stateful
CIF produces the code
static inline long unsigned int free_initmem_default(int poison)
{
char __init_begin[];
# 1350 "include/linux/mm.h"
char __init_end[];
# 1352 "include/linux/mm.h"
return free_reserved_area ( ( void *) & __init_begin , ( void *) & __init_end , poison ,
# 1353 "include/linux/mm.h"
( char *) "unused kernel" );
}
which leads to the error
include/linux/mm.h:1350:8: error: array size missing in ‘__init_begin’ include/linux/mm.h:1350:8: error: array size missing in ‘__init_end’
original code:
extern char __init_begin[], __init_end[];
Updated by Evgeny Novikov about 10 years ago
- Status changed from New to Open
Turned out to be a compiler warning that is ignored by our main verifiers.
Updated by Vadim Mutilin almost 10 years ago
Now this issue occurs in the generated code
extern char __init_begin[];
extern char __init_end[];
static inline long unsigned int free_initmem_default(int poison)
{
char __init_begin[];
char __init_end[];
return free_reserved_area ( ( void *) & __init_begin , ( void *) & __init_end , poison ,
( char *) "unused kernel" );
}
The array without size can not be allocated on the stack
Updated by Evgeny Novikov almost 10 years ago
I didn't catch, where the issue was before?
Updated by Vadim Mutilin almost 10 years ago
As I can see with a fresh look it is the same issue as before.
GCC reports the error, but CIL and CPAchecker frontends skip the issue.
Updated by Evgeny Novikov about 8 years ago
- Category set to C back-end
- Assignee set to Evgeny Novikov
- Priority changed from Normal to High
Actions