Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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