Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problems with value analysis

  • Subject: [Frama-c-discuss] Problems with value analysis
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
  • Date: Mon, 14 Dec 2009 15:55:09 +0100
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