--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on November 2014 ---
Hello, Le 05/11/2014 21:57, DUPRAT, STEPHANE a ?crit : > I don?t want the padding fields of structs in global variable at > uninitialized state. Out of curiosity, why? > I?m also using the option -initialized-padding-globals, but these > uninitialized fields are still remaining (Neon release). > Is there a workaround to have the entire location at [--..--] ? Even > for very large variables ? A possible workaround: initialize your global variables in the analysis driver using following function: """ extern int Frama_C_entropy_source; /*@ requires \valid(p + (0 .. l-1)); assigns p[0 .. l-1] \from Frama_C_entropy_source; assigns Frama_C_entropy_source \from Frama_C_entropy_source; ensures \initialized(p + (0 .. l-1)); */ void Frama_C_make_unknown(char *p, size_t l); """ For example "Frama_C_make_unknown(&my_var, 32);". I hope it helps, Best regards, david