--- layout: fc_discuss_archives title: Message 121 from Frama-C-discuss on December 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problems with value analysis



Hi,

I ran the value analysis plugin of Beryllium 2 on the code below, which produced messages that I don't understand:

- function set is invoked by set( &Ctx, -1, 0 ) in main(), which causes an out of bound access in set(). This is reported for the location in set(), where the out of bound accesss actually happens, but where it is not caused. How can the user discover the origin of the bug?

- Non termination is reported for functions set() and main(). As there are no loops in set(), is this message a bug or just a false positive?

-Boris



#define MYCTX_MAX_BUF_LEN 100

typedef struct MyCtx_s
{
    int buf[MYCTX_MAX_BUF_LEN];
} MyCtx_t;



/*@ requires \valid(pCtx) && \valid(pCtx->buf + idx);
    assigns pCtx->buf[idx];
 */
static
void set( MyCtx_t *pCtx, int idx, int x )
{
    pCtx->buf[idx] = x; // ** out of bound access
} // ** Non termination detected in  function set



int main( void )
{
    MyCtx_t Ctx;
    int x = 3;

    set( &Ctx, -1, 0 );

    return 0;
} // ** Non termination detected in  function main