--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on November 2009 ---
Hi again, Is someone know how to treat errno ? The cil create a pointer not allowed and after an access to the location. thx, St?phane src code: if (errno == 0) j=2; the cil: int *tmp ; { /*undefined sequence*/ tmp = __errno_location(); ; } /*@ assert \valid(tmp); // synthesized */ if (*tmp == 0) { j = 2; } warning: warning: out of bounds read. assert \valid(tmp); -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091107/2a4f19d9/attachment.htm