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: Claude.Marche at inria.fr (Claude Marché)
- Date: Mon, 02 Mar 2009 17:09:32 +0100
- In-reply-to: <3d13dcfc0903020703h71d0de3au20312f6464a6116e@mail.gmail.com>
- References: <3d13dcfc0903020703h71d0de3au20312f6464a6116e@mail.gmail.com>
David MENTRE wrote: > 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(), ...) right. > and even rejects certain forms (for main(): > "Bug: unsupported variadic functions"). I'm not sure about this one: does it happen if you use int main(int argc, char *argv[]) ? > First of all, what does exactly mean "No code for function xxxxxx, > default assigns generated"? You can look at ACSL manual, section 2.3.5. The point is that since a function like read() has no code given, nor contract, then it could be possible that it modifies every location in the heap. So it should be given a contract. > 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 recommend not to modify regular system headers. You can simply augment your source code with contracts for functions you use (or put them in a separate file that you #include). e.g /*@ requires \valid(buf+(0..count-1)); @ assigns errno, buf[0..count-1]; @*/ ssize_t read(int fd, void *buf, size_t count); In principle, Frama-C should be shipped with contracts for standard library functions, but this is not an easy thing to do: it is not clear at all what would be a "universal" contract for all use of thos functions... > 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 > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |
- Follow-Ups:
- [Frama-c-discuss] Best approach when specifying regular C functions from stdlib?
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] Best approach when specifying regular C functions from stdlib?
- References:
- [Frama-c-discuss] Best approach when specifying regular C functions from stdlib?
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] Best approach when specifying regular C functions from stdlib?
- Prev by Date: [Frama-c-discuss] Best approach when specifying regular C functions from stdlib?
- Next by Date: [Frama-c-discuss] Best approach when specifying regular C functions from stdlib?
- Previous by thread: [Frama-c-discuss] Best approach when specifying regular C functions from stdlib?
- Next by thread: [Frama-c-discuss] Best approach when specifying regular C functions from stdlib?
- Index(es):