You need to provide your own "file.h" file in a directory "sys" placed anywhere in the path GCC searches when pre-processing for Frama-C.
For reference, here is the implementation of sys/file.h on another system. You may also be interested in this other StackOverflow question about sys/file.h.
For Frama-C's value analysis, assigns clauses alongside the prototypes go a long way:
/*@ assigns *f \from ui, s, *fo; */
void finit(struct file *f, u_int ui, short s, void *p, struct fileops *fo);
Note that I have no idea what function finit()
does and whether the above is a correct assigns
clause for it. In fact, this is the whole point: neither does Frama-C out of the box, and since this lowish-level, lessish-portable system call is used in the code you wish to analyze, someone will have to know. I am afraid it is going to have to be you. On the plus side, you only need to provide the types, macros and function prototypes that the code you wish to analyze uses.