--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on December 2018 ---
Hi, On 12/14/18 6:17 PM, Sebastian Götte wrote: > I just upgraded to Argon and I am having issues proving the code below using memset on unsigned char pointers. So I think I've come closer to the root of this problem. I'm pretty sure the problem is that valid_or_empty contains a cast to char* in its definition. Now, a few thoughts on this and frama-c/libc/string.h in WP: * Specifying string functions such as strcmp, strchr and strlen on char* is not a bad idea. * But, realistic code is likely to use generic memory functions such as memcmp, memcpy and memset on arbitray memory. Since memsetting an arbitrary pointer is a common pattern, I think it should be well-supported by frama-c. If the core engine can't handle this yet, there should be documented workarounds. Given how common this pattern is I think this would be useful even in a beginner-level tutorial. * The current implementation of string.h is misleading in that memset et al contain casts to char* in their specs that will break anything trying to use them with non-char* input. In particular I think valid_or_empty should really be called valid_or_empty_char since it contains a cast to char* and can't handle anything else. * Similarly, in __fc_string_axiomatic.h the axiomatic definitions of the memory functions MemSet, MemChr etc. cast to char and I think that should be reflected in their names (e.g. MemSet_char). Now to my new question: I have this existing piece of C code that I would like to not modify if possible. This piece of code uses lots of uint8_t* pointers whose contents I want to memcpy, memcmp and memset, severely confusing frama-c. Is there some manual override I can use in this particular case? I'm looking for some directive to put into the code that tells frama-c "ignore the next line and assume the following holds" to tell frama-c "this variable is zero now, believe me". Best regards, Sebastian