--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on November 2009 ---
> someone know how to treat errno ? ___ 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; } ____ When I try to reproduce, I get: $ cat t.i main(){ int j; if (errno == 0) j=2; } $ /Volumes/raid/ppc/bin/toplevel.opt -print t.i Parsing t.i:3: Fatal error: Cannot resolve variable errno ... It seems to me that your pre-processor did most of the transformation here, not CIL. Could you show us the pre-processed code corresponding to your example? If your compilation platform is made of headers that insert calls to __errno_location() and of libraries that provide it, for reproducing the same context in Frama-C you have to provide the function in a separate C file that you should include in each of your analysis projects. Pascal