--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on March 2009 ---
Hello, On Mon, Mar 2, 2009 at 17:09, Claude March? <Claude.Marche at inria.fr> wrote: >> 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[]) ? Just tested: yes, same issue. Maybe the error reporting in unprecise and the faulty line is not the reported one? The used source code is: http://www.linux-france.org/~dmentre/code/dev-random-pass-gen.c In above code, I've just replaced the printf() by putchar()s. >> 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. Thank you for the precise reference to ACSL manual. I'll look at it. Maybe this should be given in the error message? > 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); Ok, I'll do that. Of course, in the meantime I've chosen the reverse path. ;-) > 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 understand. And I assume refining contracts for a specific environment might help proving properties. Many thanks for your help, Yours, d.