2021-01-15 18:02 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001093Frama-CPlug-in > jessiepublic2012-02-14 09:05
Reporterflecsim 
Assigned Tocmarche 
PrioritynormalSeveritycrashReproducibilityalways
StatusassignedResolutionopen 
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in Version 
Summary0001093: Passing multi-dimensional arrays via reference fails
DescriptionStarting 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 InformationTested 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.
TagsNo tags attached.
Attached Files
  • txt file icon 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.
    */
    
    txt file icon SamplePrograms.txt (18,509 bytes) 2012-02-13 14:05 +

-Relationships
related to 0000032assignedcmarche Internal error with assign specification on bi-dimensional arrays 
+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