--- layout: fc_discuss_archives title: Message 57 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



> 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