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

[Frama-c-discuss] Help with -wp-init-const and static evaluation of constants



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>