Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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>