--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on November 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] using errno




> 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