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: boris at yakobowski.org (Boris Yakobowski)
  • Date: Wed, 18 Jan 2012 13:42:07 +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>
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>