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



Hi,

I'm trying to use wp with alt-ergo and I'm having problems with
memsets for everything that involves more than chars.  I'm not
sure if this is just with memset or a more general problem, it's
just the first thing I notice.

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.

In the case with chars, it says it's valid for all values n that
are equal or smaller to the size.  For the case with ints only the
value 0 seems to be valid.

If I instead try to use coq I can get the "char a[2]" working, but
not the struct.

PS: Using char a; memset(&a, 0, sizeof(a)); gives me an assertion
failure.  I seem to ge very good in getting assertion failures.


Kurt