--- layout: fc_discuss_archives title: Message 4 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?




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                    |