0001093: Passing multi-dimensional arrays via reference fails

View Issue Details [ Jump to Notes ]
[ Issue History ] [ Print ]
Project
Tags
No tags attached.
Attached Files
SamplePrograms.txt (18,509 bytes) 2012-02-13 14:05
========== 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.
*/
SamplePrograms.txt (18,509 bytes) 2012-02-13 14:05
Relationships
related to
0000032
assigned
cmarche
Internal error with assign specification on bi-dimensional arrays
Relationships
Notes
There are no notes attached to this issue.
Notes
Date Modified	Username	Field	Change
Issue History
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