--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on March 2011 ---
Thanks a lot, Pascal. 2011/3/14 Pascal Cuoq <pascal.cuoq at gmail.com> > 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 > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110315/0c923463/attachment.htm>