--- layout: fc_discuss_archives title: Message 39 from Frama-C-discuss on October 2015 ---
Hi, If it can help, another possible workaround consists in rewriting the macro as a function: int MIN(int a,int b){ return ((a)<(b))?(a):(b); } then Value won't produce the alarm anymore. I guess Value is able to reduce the domain of a variable "a" after evaluating the expr "(a<b)", but not the domain of an expression "a&C" after an expr "(a&C<b)". HTH D. P.S.: don't forget #include of the builtins and the -cpp-extra-args for include dirs. > -----Message d'origine----- > De : Frama-c-discuss [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] De > la part de David MENTRE > Envoyé : jeudi 15 octobre 2015 15:32 > à: frama-c-discuss at lists.gforge.inria.fr > Objet : Re: [Frama-c-discuss] Value analysis and MIN macro > > Hello, > > Le 15/10/2015 09:16, GERARD Benoit a écrit : > > My question is the following : is this problem potentially solvable > > (by frama-c developers or may be using ACSL) > > Interesting issue! :-) > > I tried various approaches but the only one that worked for me was to put an > assert that "bound <= 10" in test2() (see attached code) and then use wp to > prove it (easy for Alt-Ergo in 21ms): > > frama-c-gui -val min-example.c -then -wp > > > or should people take the habit > > of using an intermediate variable to perform computations before using > > it in the macro (which option may ease the code review and avoid some > > errors anyway)? > > But it is true that using an intermediate variable helps Value: no need of > additional annotation and use of WP. So if you have the ability to guide > people to use this style, I would go for it. > > Best regards, > david