--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on November 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] don't want unitialized padding fields, -initialized-padding-globals



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