--- layout: fc_discuss_archives title: Message 45 from Frama-C-discuss on August 2015 ---
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>