Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Best approach when specifying regular C functions from stdlib?
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Mon, 2 Mar 2009 16:03:54 +0100
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