Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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