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

[Frama-c-discuss] defining valid memory zones



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