--- layout: fc_discuss_archives title: Message 26 from Frama-C-discuss on January 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problems with Frama-C libc



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.