--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on July 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



Hello Roderick,

Le mer. 17 juil. 2019 à 18:01, Roderick Chapman <rod at proteancode.com> a
écrit :

> Seeking help again... consider the following code:
>
> include <stddef.h>
>
> static const size_t c1 = 300;
> static const size_t c2 = c1 + 1;
>
> size_t f (size_t y)
> {
>   size_t tmp2 = (y /
> c2);
>
>   return tmp2;
> }
>
> Using Frama-C 19, I find that
>
> frama-c -wp -wp-rte -wp-init-const
>
> does _not_ prove that c2 != 0 in the division operator.  Why not? Is it
> not able to deduce that c2 == 301? This seems like a rather strange this
> not to do.
>
> Secondly, can anyone explain the exact meaning of -wp-init-const please?
> There appears to be no mention of it at all in the 19.0 WP manual...
>

 I've made a few quick experiments, and I suspect that as long as c1 does
not appear explicitly in the body of f, WP does not attempt at making sense
of this c1+1 expression it gets as the value of c2 (if you examine the
goal, it is of the form to_uint32(1 + c1_0) != 0, but you don't have any
hypothesis saying c1 = of_uint32 300). Fortunately, this can be easily
overcome: just add an assertion

//@ assert c1 == 300;

at the beginning of the function and everything gets proved.

I've also tried to play with the -constfold option of the kernel, but
apparently it only operates inside function bodies and not in global
initializers. I'll take that as a feature wish.

Regarding the WP manual, I'll let the WP maintainers themselves give a
proper answer.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile
-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190718/9acfac42/attachment.html>