--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on March 2009 ---
Hello, I'm starting to look at how I might use the Frama-C framework and the Jessie plugin on small C programs. In those programs, I'm using regular K&R standard library functions, typically: if (read(rand_fd, &x, 1) <= 0) { if (errno == EINTR) continue; perror("read"); exit(EXIT_FAILURE); or: int main(void) As expected, Frama-C / Jessie does not know much about those functions (read(), perror(), ...) and even rejects certain forms (for main(): "Bug: unsupported variadic functions"). First of all, what does exactly mean "No code for function xxxxxx, default assigns generated"? Secondly, I would like to define more specific contracts on those library functions (requires, ensures, ...). How should I proceed? Should I define my own header, with a copy/paste of used system definitions (size_t, open(), ...), enhanced with specific contracts? Or should I simply include regular system headers and enhance them with my additional contract? In that case, how can I avoid errors like the one on main() seen as variadic function? I am asking this because I assume certain approaches are more scalable and maintainable when you want to verify a lot of development code made for a specific development environment. I hope I'm clear. ;-) Sincerely yours, david