--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on March 2009 ---
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 |