--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on September 2015 ---
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