--- layout: fc_discuss_archives title: Message 5 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



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

Many thanks,

  Rod


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190717/9591c74c/attachment.html>