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

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