--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on March 2009 ---
Hello, I join to this email the two files currently used: dev-random-pass-gen.c and check_specs.h. My system is a Debian Lenny 5.0 Linux system, but I think the system headers should be similar if not identical to Ubuntu 8.04. On Tue, Mar 3, 2009 at 10:08, David MENTRE <dmentre at linux-france.org> wrote: > On Tue, Mar 3, 2009 at 09:28, Virgile Prevosto <virgile.prevosto at cea.fr> wrote: > [ regarding undefined contracts. ] >> better to give an appropriate contract to each prototype which has no >> associated definition. > > Ok, I'll do that. Following this approach (appropriate contract to system functions), I have two issues: 1. I still have a bug with main(): dev-random-pass-gen.c:71: Bug: unsupported variadic functions Dropping definition of function main I have followed you recommendation, i.e. I declare main() as: int main(int argc, char *argv[]) This is annoying, as I would like to analyse main(). :-) I think I can go around this by defining a second main2() and analysing that with "-main", but I would like to know if I made a mistake. 2. for read(), the system declaration is "ssize_t read(int fd, void *buf, size_t count);". However, the "buf" pointer is to void, that Frama-C does not support. For example I cannot declare "requires \valid(buf);". And I can't change the declaration to "char *" as it would not match the system declaration. Any recommendation? I could copy/past the code of read() and redefine it, but I fear I could just postpone the issue to another function. Sincerely yours, d. -------------- next part -------------- A non-text attachment was scrubbed... Name: dev-random-pass-gen.c Type: application/octet-stream Size: 4951 bytes Desc: not available Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090303/65b524ff/attachment.obj -------------- next part -------------- A non-text attachment was scrubbed... Name: check_specs.h Type: application/octet-stream Size: 503 bytes Desc: not available Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090303/65b524ff/attachment-0001.obj