--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on December 2018 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



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;
> }
>