--- layout: fc_discuss_archives title: Message 38 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



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;

}