| Anonymous | Login | Signup for a new account | 2019-05-21 16:06 CEST |  |
| Main | My View | View Issues | Change Log | Roadmap | Repositories |
| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
| 0001093 | Frama-C | Plug-in > jessie | public | 2012-02-13 14:05 | 2012-02-14 09:05 | ||||||||
| Reporter | flecsim | ||||||||||||
| Assigned To | cmarche | ||||||||||||
| Priority | normal | Severity | crash | Reproducibility | always | ||||||||
| Status | assigned | Resolution | open | ||||||||||
| Platform | OS | OS Version | |||||||||||
| Product Version | Frama-C Nitrogen-20111001 | ||||||||||||
| Target Version | Fixed in Version | ||||||||||||
| Summary | 0001093: Passing multi-dimensional arrays via reference fails | ||||||||||||
| Description | Starting from the simple function #define MAX_SIZE_X 10 typedef int AnArray[MAX_SIZE_X]; void FillArray(AnArray *paTarget, int Value) { int x = 0; for (x = 0; x < MAX_SIZE_X; x++) { (*paTarget)[x] = Value; } } the code above is accepted by Jessie and can be verified (annotations removed for brevity here), but as AnArray is extended to two or more dimensions (typedef int AnArray[MAX_SIZE_X][MAX_SIZE_Y]...) - and the filling loops adapted to match - jessie crashes on loading the source file. | ||||||||||||
| Additional Information | Tested with Frama-C/Nitrogen, why-2.30 and why3-0.71 compiled in cygwin. Loading the code samples in "regular" Frama-C GUI or using WP plug-in does not cause a crash. I actually encountered this when analyzing the tree-dimensional case (parallelized matrix operations); this is the smallest form i found which shows the problem. More variants can be created, e.g. by moving one array dimension from the typedef into the actual argument (AnArray *paTarget[MAX_SIZE_X], int Value). Attached file contains four C sources to demonstrate the problem (to be split at the comment boxes), accompanied by their stacktraces. | ||||||||||||
| Tags | No tags attached. | ||||||||||||
| Attached Files |  SamplePrograms.txt [^] (18,509 bytes) 2012-02-13 14:05 [Show Content] [Hide Content]========== One-dimensional array, does not crash ==========
#define MAX_SIZE_X 10
typedef int AnArray[MAX_SIZE_X];
/*@requires \valid(paTarget);
@requires \valid_range(*paTarget, 0, MAX_SIZE_X);*/
void FillArray(AnArray *paTarget, int Value)
{
int x = 0;
/*@loop invariant x >= 0;
@loop variant MAX_SIZE_X - x; */
for (x = 0; x < MAX_SIZE_X; x++)
{
/*@assert x < MAX_SIZE_X; */
(*paTarget)[x] = Value;
}
}
/* Jessie gets everything "green" on the program above
with alt-ergo 0.94, no problems */
/**************************************************************************
* Two-dimensional array, crashes *
**************************************************************************/
#define MAX_SIZE_X 10
#define MAX_SIZE_Y 11
typedef int AnArray[MAX_SIZE_X][MAX_SIZE_Y];
void FillArray(AnArray *paTarget, int Value)
{
int x = 0;
int y = 0;
/*@loop invariant x >= 0;
@loop variant MAX_SIZE_X - x; */
for (x = 0; x < MAX_SIZE_X; x++)
{
/*@loop invariant y >= 0;
@loop variant MAX_SIZE_Y - y;
*/
for (y = 0; y < MAX_SIZE_Y; y++)
{
(*paTarget)[x][y] = Value;
}
}
}
/* Jessie crashes with
D:\Frama-C>frama-c.exe -pp-annot -jessie test.c
[kernel] preprocessing with "C:/tool/Cygwin/bin/gcc.exe -C -E -dD test.c"
[jessie] Starting Jessie translation
test.c:20:[jessie] failure: Unexpected lval (*((paTarget + x)->intM))[y]
[kernel] The full backtrace is:
Raised at file "src/kernel/log.ml", line 509, characters 30-31
Called from file "src/kernel/log.ml", line 503, characters 9-16
Re-raised at file "src/kernel/log.ml", line 506, characters 15-16
Called from file "interp.ml", line 1817, characters 29-40
Called from file "interp.ml", line 1980, characters 17-30
Called from file "list.ml", line 62, characters 22-25
Called from file "interp.ml", line 2156, characters 36-66
Called from file "interp.ml", line 2111, characters 17-43
Called from file "list.ml", line 62, characters 22-25
Called from file "interp.ml", line 2156, characters 36-66
Called from file "interp.ml", line 2162, characters 32-54
Called from file "interp.ml", line 2108, characters 41-49
Called from file "list.ml", line 62, characters 22-25
Called from file "interp.ml", line 2156, characters 36-66
Called from file "interp.ml", line 2111, characters 17-43
Called from file "list.ml", line 62, characters 22-25
Called from file "interp.ml", line 2156, characters 36-66
Called from file "interp.ml", line 2162, characters 32-54
Called from file "interp.ml", line 2108, characters 41-49
Called from file "list.ml", line 62, characters 22-25
Called from file "interp.ml", line 2156, characters 36-66
Called from file "interp.ml", line 2590, characters 40-71
Called from file "list.ml", line 62, characters 22-25
Called from file "interp.ml", line 2716, characters 27-66
Called from file "register.ml", line 149, characters 16-32
Called from file "register.ml", line 290, characters 6-12
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 36, characters 4-20
Called from file "src/kernel/cmdline.ml", line 723, characters 2-9
Called from file "src/kernel/cmdline.ml", line 200, characters 4-8
Plug-in jessie aborted because of internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Nitrogen-20111001.
*/
/**************************************************************************
* Three-dimensional array, crashes (with another error message) *
**************************************************************************/
#define MAX_SIZE_X 10
#define MAX_SIZE_Y 11
#define MAX_SIZE_Z 12
typedef int AnArray[MAX_SIZE_X][MAX_SIZE_Y][MAX_SIZE_Z];
void FillArray(AnArray *paTarget, int Value)
{
int x = 0;
int y = 0;
int z = 0;
/*@loop invariant x >= 0;
@loop variant MAX_SIZE_X - x; */
for (x = 0; x < MAX_SIZE_X; x++)
{
/*@loop invariant y >= 0;
@loop variant MAX_SIZE_Y - y;
*/
for (y = 0; y < MAX_SIZE_Y; y++)
{
/*@loop invariant z >= 0;
@loop variant MAX_SIZE_Z - z;
*/
for (z = 0; z < MAX_SIZE_Z; z++)
{
(*paTarget)[x][y][z] = Value;
}
}
}
}
/* Jessie crashes with
[kernel] preprocessing with "C:/tool/Cygwin/bin/gcc.exe -C -E -dD test.c"
[jessie] Starting Jessie translation
test.c:27:[kernel] failure: typeOfLval: Mem on a non-pointer ((*paTarget)[x])
[kernel] The full backtrace is:
Raised at file "src/kernel/log.ml", line 509, characters 30-31
Called from file "src/kernel/log.ml", line 503, characters 9-16
Re-raised at file "src/kernel/log.ml", line 506, characters 15-16
Called from file "common.ml", line 907, characters 32-42
Called from file "common.ml", line 914, characters 26-42
Called from file "cil/src/cil.ml", line 1452, characters 15-31
Called from file "cil/src/cil.ml", line 2256, characters 12-53
Called from file "cil/src/cil.ml", line 2347, characters 16-22
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2392, characters 17-25
Called from file "cil/src/cil.ml", line 1489, characters 13-16
Called from file "cil/src/cil.ml", line 1534, characters 24-57
Called from file "cil/src/cil.ml", line 2380, characters 5-52
Called from file "cil/src/cil.ml", line 2506, characters 14-21
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2424, characters 5-86
Called from file "cil/src/cil.ml", line 1489, characters 13-16
Called from file "cil/src/cil.ml", line 2558, characters 16-40
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2511, characters 11-19
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2424, characters 5-86
Called from file "cil/src/cil.ml", line 1489, characters 13-16
Called from file "cil/src/cil.ml", line 2558, characters 16-40
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2484, characters 11-19
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2424, characters 5-86
Called from file "cil/src/cil.ml", line 1489, characters 13-16
Called from file "cil/src/cil.ml", line 2558, characters 16-40
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2511, characters 11-19
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2424, characters 5-86
Called from file "cil/src/cil.ml", line 1489, characters 13-16
Called from file "cil/src/cil.ml", line 2558, characters 16-40
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2484, characters 11-19
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2424, characters 5-86
Called from file "cil/src/cil.ml", line 1489, characters 13-16
Called from file "cil/src/cil.ml", line 2558, characters 16-40
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2511, characters 11-19
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2424, characters 5-86
Called from file "cil/src/cil.ml", line 1489, characters 13-16
Called from file "cil/src/cil.ml", line 2558, characters 16-40
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2484, characters 11-19
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2424, characters 5-86
Called from file "cil/src/cil.ml", line 1489, characters 13-16
Called from file "cil/src/cil.ml", line 2558, characters 16-40
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2771, characters 14-39
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2746, characters 5-91
Called from file "cil/src/cil.ml", line 2822, characters 16-38
Called from file "cil/src/cil.ml", line 1489, characters 13-16
Called from file "cil/src/cil.ml", line 1534, characters 24-57
Called from file "cil/src/cil.ml", line 2816, characters 5-53
Called from file "cil/src/cil.ml", line 8413, characters 17-37
Called from file "cil/src/cil.ml", line 8420, characters 3-20
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 8437, characters 15-39
Called from file "norm.ml", line 1873, characters 19-35
Called from file "register.ml", line 131, characters 4-23
Called from file "register.ml", line 290, characters 6-12
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 36, characters 4-20
Called from file "src/kernel/cmdline.ml", line 723, characters 2-9
Called from file "src/kernel/cmdline.ml", line 200, characters 4-8
Frama-C aborted because of internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Nitrogen-20111001.
*/
/**************************************************************************
* Four-dimensional array, crashes (like the three-dimensional one) *
**************************************************************************/
#define MAX_SIZE_X 10
#define MAX_SIZE_Y 11
#define MAX_SIZE_Z 12
#define MAX_SIZE_T 13
typedef int AnArray[MAX_SIZE_X][MAX_SIZE_Y][MAX_SIZE_Z][MAX_SIZE_T];
void FillArray(AnArray *paTarget, int Value)
{
int x = 0;
int y = 0;
int z = 0;
int t = 0;
/*@loop invariant x >= 0;
@loop variant MAX_SIZE_X - x; */
for (x = 0; x < MAX_SIZE_X; x++)
{
/*@loop invariant y >= 0;
@loop variant MAX_SIZE_Y - y;
*/
for (y = 0; y < MAX_SIZE_Y; y++)
{
/*@loop invariant z >= 0;
@loop variant MAX_SIZE_Z - z;
*/
for (z = 0; z < MAX_SIZE_Z; z++)
{
for (t = 0; t < MAX_SIZE_T; t++)
{
(*paTarget)[x][y][z][t] = Value;
}
}
}
}
}
/* Jessie crashes with:
D:\Frama-C>frama-c.exe -pp-annot -jessie test.c
[kernel] preprocessing with "C:/tool/Cygwin/bin/gcc.exe -C -E -dD test.c"
[jessie] Starting Jessie translation
test.c:31:[kernel] failure: typeOfLval: Mem on a non-pointer ((*paTarget)[x])
[kernel] The full backtrace is:
Raised at file "src/kernel/log.ml", line 509, characters 30-31
Called from file "src/kernel/log.ml", line 503, characters 9-16
Re-raised at file "src/kernel/log.ml", line 506, characters 15-16
Called from file "cil/src/cil.ml", line 3996, characters 24-37
Called from file "common.ml", line 907, characters 32-42
Called from file "common.ml", line 914, characters 26-42
Called from file "cil/src/cil.ml", line 1452, characters 15-31
Called from file "cil/src/cil.ml", line 2256, characters 12-53
Called from file "cil/src/cil.ml", line 2347, characters 16-22
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2392, characters 17-25
Called from file "cil/src/cil.ml", line 1489, characters 13-16
Called from file "cil/src/cil.ml", line 1534, characters 24-57
Called from file "cil/src/cil.ml", line 2380, characters 5-52
Called from file "cil/src/cil.ml", line 2506, characters 14-21
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2424, characters 5-86
Called from file "cil/src/cil.ml", line 1489, characters 13-16
Called from file "cil/src/cil.ml", line 2558, characters 16-40
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2511, characters 11-19
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2424, characters 5-86
Called from file "cil/src/cil.ml", line 1489, characters 13-16
Called from file "cil/src/cil.ml", line 2558, characters 16-40
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2484, characters 11-19
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2424, characters 5-86
Called from file "cil/src/cil.ml", line 1489, characters 13-16
Called from file "cil/src/cil.ml", line 2558, characters 16-40
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2511, characters 11-19
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2424, characters 5-86
Called from file "cil/src/cil.ml", line 1489, characters 13-16
Called from file "cil/src/cil.ml", line 2558, characters 16-40
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2484, characters 11-19
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2424, characters 5-86
Called from file "cil/src/cil.ml", line 1489, characters 13-16
Called from file "cil/src/cil.ml", line 2558, characters 16-40
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2511, characters 11-19
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2424, characters 5-86
Called from file "cil/src/cil.ml", line 1489, characters 13-16
Called from file "cil/src/cil.ml", line 2558, characters 16-40
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2484, characters 11-19
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2424, characters 5-86
Called from file "cil/src/cil.ml", line 1489, characters 13-16
Called from file "cil/src/cil.ml", line 2558, characters 16-40
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2511, characters 11-19
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2424, characters 5-86
Called from file "cil/src/cil.ml", line 1489, characters 13-16
Called from file "cil/src/cil.ml", line 2558, characters 16-40
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2484, characters 11-19
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2424, characters 5-86
Called from file "cil/src/cil.ml", line 1489, characters 13-16
Called from file "cil/src/cil.ml", line 2558, characters 16-40
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2771, characters 14-39
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2746, characters 5-91
Called from file "cil/src/cil.ml", line 2822, characters 16-38
Called from file "cil/src/cil.ml", line 1489, characters 13-16
Called from file "cil/src/cil.ml", line 1534, characters 24-57
Called from file "cil/src/cil.ml", line 2816, characters 5-53
Called from file "cil/src/cil.ml", line 8413, characters 17-37
Called from file "cil/src/cil.ml", line 8420, characters 3-20
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 8437, characters 15-39
Called from file "norm.ml", line 1873, characters 19-35
Called from file "register.ml", line 131, characters 4-23
Called from file "register.ml", line 290, characters 6-12
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 36, characters 4-20
Called from file "src/kernel/cmdline.ml", line 723, characters 2-9
Called from file "src/kernel/cmdline.ml", line 200, characters 4-8
Frama-C aborted because of internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Nitrogen-20111001.
*/
| ||||||||||||
 Relationships |
||||||
|
||||||
 Relationships |
|
Notes |
|
| There are no notes attached to this issue. |
|
Notes |
|
Issue History |
|||
| Date Modified | Username | Field | Change |
| 2012-02-13 14:05 | flecsim | New Issue | |
| 2012-02-13 14:05 | flecsim | Status | new => assigned |
| 2012-02-13 14:05 | flecsim | Assigned To | => cmarche |
| 2012-02-13 14:05 | flecsim | File Added: SamplePrograms.txt | |
| 2012-02-14 09:05 | virgile | Relationship added | related to 0000032 |
|
Issue History |
| Copyright © 2000 - 2019 MantisBT Team |
|