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