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