--- layout: fc_discuss_archives title: Message 18 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



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>