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



On Monday, March 14, 2011, kevin fu <kevin09fjw at gmail.com> wrote:
> 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.

You are talking about the initial values of the entry point's
arguments (and of global variables if using option -lib-entry) in the
value analysis.

> ?? ? 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.

You need to use -lib-entry if you want globals to be treated like
this. Also, the shape of initial values that you describe is only
exactly as you describe in the Frama-C Carbon version. In earlier
versions, arrays were treated uniformly, with no difference between
the first few cells and the remaining ones.

Pascal