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

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>