--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on November 2014 ---
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>