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] Problems with Frama-C libc

  • Subject: [Frama-c-discuss] Problems with Frama-C libc
  • From: anne.pacalet at free.fr (Anne Pacalet)
  • Date: Wed, 18 Jan 2012 11:12:10 +0100
  • In-reply-to: <CABbVA-Aptsb4m3=JdO+2mfJh-G-F8icf4yoSKKxSPFvfNjJ3HQ@mail.gmail.com>
  • References: <4F1693C8.9040409@free.fr> <CABbVA-Aptsb4m3=JdO+2mfJh-G-F8icf4yoSKKxSPFvfNjJ3HQ@mail.gmail.com>
Hello Pascal and Boris,

Le 18/01/2012 10:52, Pascal Cuoq wrote :
 > The headers in `frama-c -print-path`/libc are, literally, untested.
 > They should be assumed to contain syntax errors or unsatisfiable
 > specifications until shown otherwise.

Ok: this is very clear ;-)

 > Le 18/01/2012 11:03, Boris Yakobowski wrote :
> This actually works in the development version, with the same
> specifications as in Nitrogen.

Good news ! I have to wait for the next version then !

> I'm however puzzled as to why this is
> so: most of the changes in the handling of assigns clauses occurred
> before Nitrogen, and Value will not interpret anything else in the
> specification of strncpy. I will try to have a closer look as soon as
> possible.

Ok.

Thank you very much to both of you,

Anne.