--- layout: fc_discuss_archives title: Message 39 from Frama-C-discuss on October 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Value analysis and MIN macro



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