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] static arrays

  • Subject: [Frama-c-discuss] static arrays
  • From: boris at yakobowski.org (Boris Yakobowski)
  • Date: Wed, 26 Aug 2015 15:50:05 +0200
  • In-reply-to: <CAOH62JhX-4Sj0cHbA+AAzAPL5WijRf7cRcyW=g-Za8hYORTYBA@mail.gmail.com>
  • References: <CAL+X0enWOro4KtpXUCBee4=-SG4LNYht8X=VgBad+tjWVsckKQ@mail.gmail.com> <CAOH62JhX-4Sj0cHbA+AAzAPL5WijRf7cRcyW=g-Za8hYORTYBA@mail.gmail.com>
Hi,

On Tue, Aug 18, 2015 at 4:53 AM, Pascal Cuoq <pascal.cuoq at gmail.com> wrote:

>
> WP does not appear to take advantage of const qualifiers, according to
> your results. I will leave you the care of submitting that as a feature
> wish if you think that it is important.
>
>
>
To elaborate a bit on this point, this is already possible with option
-wp-init-const -- thanks to which all four assertions are proven. If I
remember correctly, it is not active by default so as not to flood the goal
with possibly useless assertions about the initializers.

Hope this helps,


-- 
Boris
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150826/3c603289/attachment.html>