Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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