Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problems in Argon with memset on unsigned char arrays

  • Subject: [Frama-c-discuss] Problems in Argon with memset on unsigned char arrays
  • From: jaseg at physik.tu-berlin.de (Sebastian Götte)
  • Date: Fri, 14 Dec 2018 18:17:16 +0900
Hi,

I just upgraded to Argon and I am having issues proving the code below using memset on unsigned char pointers. In Chlorine the proof worked with a simple \valid on the arrays, in Argon I changed that to valid_or_empty but it doesn't work.

In the code below this mail, alt-ergo can prove the valid_s require on baz but not on bar. I'm a little confused here, as the function's requires are translated to
> requires valid_or_empty((void *)st->bar, (unsigned int)32);
> requires valid_or_empty((void *)st->baz, (unsigned int)32);

...which is precisely the require it can't prove. Since both memset and valid_or_empty are taking a void* anyway, why should the type it was casted from matter in the first place?

I'm getting a similar problem on memcpy it seems, but I haven't looked into that any further.

Best regards and thanks for your always helpful comments,
Sebastian

> #include <string.h>
> 
> struct foo {
>     unsigned char *bar;
>       signed char *baz;
> };
> 
> /*@ requires \valid(st);
>     requires \separated(st, st->bar, st->baz);
>  
>     requires valid_or_empty(st->bar, (unsigned int)32);
>     requires valid_or_empty(st->baz, (unsigned int)32);
> 
>     assigns st->baz[0..31], st->bar[0..31];
>  */
[the following code is pasted from frama-c-gui to include the preconditions]
> int generate_identity_key(struct foo *st)
> {
>   int __retres;
>   /* preconditions of memset:
>      requires valid_s: valid_or_empty((void *)st->bar, (unsigned int)32); */ // <-- this isn't proven
>   /*@ assert rte: mem_access: \valid_read(&st->bar); */
>   memset((void *)st->bar,0,(unsigned int)32);
>   /* preconditions of memset:
>      requires valid_s: valid_or_empty((void *)st->baz, (unsigned int)32); */ // <-- this is proven
>   /*@ assert rte: mem_access: \valid_read(&st->baz); */
>   memset((void *)st->baz,0,(unsigned int)32);
>   __retres = 0;
>   return __retres;
> }
>