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