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



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