--- layout: fc_discuss_archives title: Message 26 from Frama-C-discuss on January 2012 ---
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.