--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on December 2018 ---
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; > } >