--- layout: fc_discuss_archives title: Message 57 from Frama-C-discuss on September 2009 ---
> I don't succeed in defining valid memory zones with the \valid() > function in requires clauses. > The value analysis considers that f1 don't terminate. > > test1.c:14:[kernel] warning: out of bounds read. assert \valid(adr+8); > test1.c:16:[kernel] warning: non termination detected in function f1 > > > /*@ requires \valid(adr+ (0..100)); > requires \valid(adr+8); > */ > int f1(const char * const adr) > { > char buf; > //@ assert \valid(adr+ (0..100)); > //@ assert \valid(adr+8); > buf = *(adr+8); > return buf; > } > > With this second trial, I got the assert verified, but even assertions > are appearing as dead-code ! > > test1.c:12:[value] Assertion got status valid. > test1.c:13:[value] Assertion got status valid. > test1.c:17:[kernel] warning: non termination detected in function f1 > > char tab1[100]; > /*@ requires \valid(adr+ (0..100)); > requires \valid(adr+8); > requires adr == &(tab1[0]); > */ > int f1(const char * const adr) > { > char buf; > //@ assert \valid(adr+ (0..100)); > //@ assert \valid(adr+8); > buf = *(adr+8); > return buf; > } > > > Perhaps, I didn't found the good option, > I use : frama-c -lib-entry -context-valid-pointers -main f1 -val file.c > > Thanks in advance for your help, > > St?phane > hi Steph, With Pascal's explanations in mind, you can either rewrite your example as: /* command: frama-c -val str1.c -main f1 -lib-entry -context-width 9 -context-valid-pointers */ int f1(const char * const adr) { char buf; //@ assert \valid(adr+(0..8)); buf = *(adr+8); return buf; } with the drawback that ALL pointer parameters refer to (independent) blocks of the same size, or like this: /* command: frama-c-gui -val str.c */ char tab1[101]; int f1(const char * const adr) { char buf; //@ assert \valid(adr+ (0..100)); buf = *(adr+8); return buf; } int main() { return f1(&tab1); } which is probably more flexible. Best, Armand