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

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

-------------- next part --------------
#include "__fc_builtin.h"

#define MIN(a,b) (((a)<(b))?(a):(b))

 

void test1()

{

   char tab[10];

   int i, a = Frama_C_interval(0,1000), b = 10;

 

   int bound = MIN(a,b);

   for ( i = 0 ; i < bound ; i ++ )

     tab[i] = i;

}

 

void test2()

{

   char tab[10];

   int i, a = Frama_C_interval(0,1000), b = 10;

   int bound = MIN(a & 0xFF,b);
   //@ assert bound <= 10;
   for ( i = 0 ; i < bound ; i ++ )

     tab[i] = i;

}

 

void test3()

{

   char tab[10];

   int i, a = Frama_C_interval(0,1000), b = 10;

 

   int atemp = a & 0xFF;

   int bound = MIN(atemp,b);

   for ( i = 0 ; i < bound ; i ++ )

     tab[i] = i;

}

 

int main()

{

   test1();

   test2();

   test3();

   return 0;

}