--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on March 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] problem about initial values for pointer type



Hello,
     I've been told a pointer type is assumed to point at the beginning of
an array of two elements. And all remaining cells are made to contain a
non-deterministic superposition of the first ones.
     but, when I define an global array ----- int *(array[5]) ------ frama-c
tells me that the array is initialed to array[0..4] {0; }, not something
like array[0] {‌{&NULL, &s_b_0_t}‌} which i think it should be.

     Can somebody explain this problem ?

     thank u.


kevin
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110314/539f22de/attachment.htm>