--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on November 2009 ---
Hi Pascal, I aggree with you, it's better to send a file exemple that works. But your answer is rigth, I've solved my problem with that short implementation of errno: int Ri_errno; int * __errno_location (void) { Ri_errno = Frama_C_interval (0 , 255); return &Ri_errno; } thx, St?phane Le samedi 07 novembre 2009 ? 12:22 +0100, CUOQ Pascal a ?crit : > > > 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 -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091107/9849fe4b/attachment.htm