--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on July 2019 ---
Hello, Le jeu. 18 juil. 2019 à 10:59, Roderick Chapman <rod at proteancode.com> a écrit : > On 18/07/2019 07:14, Virgile Prevosto wrote: > > //@ assert c1 == 300; > > at the beginning of the function and everything gets proved. > > That seems to work, but is unacceptable - the whole point of having named > constants (especially a set of them where the values depend on each other) > is to avoid having literal "magic numbers" all over the place. > Many thanks for this valuable feedback. My point has never been to pretend that this was a perfect solution, only that, to the best of my knowledge, this is the only sensible workaround that can be used with the current version of Frama-C[1]. The second part of my answer hinted at what could be a longer term solution, but this requires an extension of the Frama-C kernel. As always, such an extension may or may not materialize in the next release depending on how well it aligns with the overall objectives of the projects that fund the development of the platform (and/or on the willingness of external contributor(s) to work on that). [1] As a matter of fact, it is also possible to use some kind of lemma function to do the same trick. It still forces you to rewrite a 300 somewhere, but only once and can be kept close to the definition of c1: #include <stddef.h> static const size_t c1 = 300; /*@ ghost /@ assigns \nothing; ensures c1 == 300; @/ void g() {} */ static const size_t c2 = c1 + 1; size_t f (size_t y) { //@ ghost g(); size_t tmp2 = (y / c2); return tmp2; } 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/803fb325/attachment.html>