--- layout: fc_discuss_archives title: Message 51 from Frama-C-discuss on September 2009 ---
Hi, 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 -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090923/e60d1809/attachment.htm