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



On Wed, Jan 18, 2012 at 11:03 AM, Boris Yakobowski <boris at yakobowski.org> wrote:
> This actually works in the development version, with the same
> specifications as in Nitrogen. 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.

Hi again. After further investigation, this is a variant of bug 996,
that was (privately) reported some times ago. It occurs when doing
some reductions on incorrect pointers, those reductions being in fact
illegal according to the ACSL specification. Hopefully, applying the
attached patch should fix your problem.

-- 
Boris
-------------- next part --------------
A non-text attachment was scrubbed...
Name: patch-996
Type: application/octet-stream
Size: 654 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120118/011b6421/attachment.obj>