--- layout: fc_discuss_archives title: Message 19 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



It works for me. Did you provide the specification for Frama_C_make_unknown
that David gave? It doesn't work if it's not provided.

~ $ cat t.c

int Frama_C_entropy_source;


typedef unsigned long size_t;


/*@ 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);


typedef struct {

  char a[3];

  int b;

} T_S1;


typedef T_S1 T_T1[1000];


T_T1 Gtab1;

T_T1 Gtab_witness;

T_S1 G2;


void f1(T_S1* p1)

{

  Frama_C_make_unknown(Gtab1, sizeof(T_T1));

  Frama_C_make_unknown(&G2, sizeof(T_S1));

  Frama_C_dump_each();

}


~ $ frama-c -val t.c -main f1

?

[value] DUMPING STATE of file t.c line 27

        Frama_C_entropy_source ? [--..--]

        Gtab1[0..999] ? [--..--]

        Gtab_witness[0..999] ? {0}

        G2 ? [--..--]

        p1 ? {‌{ NULL ; &S_p1[0] }‌}

        S_p1[0].a[0..2] ? [--..--]

            [0].[bits 24 to 31] ? UNINITIALIZED

            {[0].b; [1].a[0..2]} ? [--..--]

            [1].[bits 24 to 31] ? UNINITIALIZED

            [1].b ? [--..--]

        =END OF DUMP==
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20141106/5f95426c/attachment.html>