--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on December 2018 ---
Hello, The addition of valid_or_empty was done to ensure that the special case when the length parameter is 0 (e.g. in memcpy) is still properly detected by Frama-C: a valid pointer is still necessary (C11, §7.24.1.2), even if no data is copied. Unfortunately, there is no way in ACSL to check it for a void* pointer without casting it to a pointer to a datatype of size 1. Following C11, §7.24.1.3, strictly speaking, the cast to "char*" might have been written "unsigned char*". For WP, however, this would not change anything; the cast would still be present. I am unable to give detailed information about WP support, but at least temporarily, reverting to the specifications from Frama-C 17 should be fine, unless you know your code is likely to include zero-length memcpy and similar calls with possibly invalid pointers (in practice, this is a rare situation). Concerning your new question: not being well-versed in WP, the only suggestion I could think of would be an ugly hack consisting in using the C preprocessor and the predefined macro __FRAMAC__: #ifndef __FRAMAC__  // original code #else  bzero(p, n); // code that will be seen only by Frama-C #endif This would be a completely generic way to ensure the code still compiles as before, but produces a different behavior when analyzed by Frama-C. Obviously, one must then ensure that both behave the same way, etc. On 16/12/2018 04:03, Sebastian Götte wrote: > 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 > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss -- André Maroneze Researcher/Engineer CEA/List Software Reliability and Security Laboratory -------------- next part -------------- A non-text attachment was scrubbed... Name: smime.p7s Type: application/pkcs7-signature Size: 3797 bytes Desc: S/MIME Cryptographic Signature URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20181221/d5f36e28/attachment.bin>