--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on September 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] memset and non-chars



Hello,

Le 2015-09-04 19:18, Kurt Roeckx a écrit :
> For instance the following things can be checked:
> char a[2]; memset(a, 0, sizeof(a));
> struct b { char c[2]; } d; memset(&d, 0, sizeof(d));
>
> But if you change the char to int, it can no longer say it's
> valid.

I would say it is related to the memory model. Possible explanation: 
memset() expects char and giving to it violate this assumption. I can at 
least prove the second memset() (on integer struct) with Typed+cast 
memory model.

   frama-c-gui -wp -wp-rte -wp-model Typed+cast kurt-memset.c

"""
#include <string.h>

void main(void)
{
   char a_c[2];
   struct b_c { char c[2]; } d_c;

   memset(a_c, 0, sizeof(a_c));
   memset(&d_c, 0, sizeof(d_c));

   int a_i[2];
   struct b_i { int c[2]; } d_i;

   memset(a_i, 0, sizeof(a_i));
   memset(&d_i, 0, sizeof(d_i));
}
"""

You have some warnings. I cannot say if they are harmful or not.

kurt-memset.c:9:[wp] warning: Cast with incompatible pointers types 
(source: b*) (target: sint8*)
kurt-memset.c:7:[wp] warning: Cast with incompatible pointers types 
(source: sint32*) (target: sint8*)

I think we have discussed such warnings on this list, but can't remember 
when.

On this code you'll have more success with Value analysis (-val).
   frama-c-gui -val kurt-memset.c

Best regards,
david