--- layout: fc_discuss_archives title: Message 68 from Frama-C-discuss on December 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] how padding are introduced by Frama-C



Hi,

Here is an exemple where padding has a consequence on warnings.

These two structures differs only from the type of the first field.
typedef struct {
  int i;
  T_TAB t;
} T_S1;

typedef struct {
  char c;
  T_TAB t;
} T_S2;

The second one cause problem when used as in the attached exemple and I
don't know why.
Access to the field t in a loop causes a warning in the second case and
not in the first one.

test3.c:32:[kernel] warning: accessing uninitialized left-value *((char
*)(tV2[id].t) + i): assert(TODO)

Could someone explain me what happens.

thanks in advance,

St?phane




-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091207/7b8a43b5/attachment.htm 
-------------- next part --------------
A non-text attachment was scrubbed...
Name: test3.c
Type: text/x-csrc
Size: 466 bytes
Desc: not available
Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091207/7b8a43b5/attachment.c