--- layout: fc_discuss_archives title: Message 121 from Frama-C-discuss on December 2009 ---
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