--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on March 2011 ---
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