| 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