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

[Frama-c-discuss] Best approach when specifying regular C functions from stdlib?



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