--- layout: fc_discuss_archives title: Message 45 from Frama-C-discuss on August 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] static arrays



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>