--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on August 2019 ---
Thanks for the feedback, As Virgile said, this is a bug in our heuristics responsible for removing all « unused » definitions from the proof context. Sorry for the inconvenience. Regarding the init-const option, it is very likely to set by default (and removed) in future versions, since assigning a « const » variable is considered to be an error by the kernel. Regards, L. > Le 18 juil. 2019 à 10:59, Roderick Chapman <rod at proteancode.com> a écrit : > > On 18/07/2019 07:14, Virgile Prevosto wrote: >> //@ assert c1 == 300; >> >> at the beginning of the function and everything gets proved. > That seems to work, but is unacceptable - the whole point of having named constants (especially a set of them where the values depend on each other) is to avoid having literal "magic numbers" all over the place. > > - Rod > > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190819/fa3d6199/attachment.html>