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

  • Subject: [Frama-c-discuss] Value analysis and MIN macro
  • From: benoit.gerard at intradef.gouv.fr (GERARD Benoit)
  • Date: Thu, 15 Oct 2015 07:16:23 +0000
  • In-reply-to: <E453609450422C4F8EB7A1BA1806686010070EE0@INF31BRUZ--WM15.DR-RES.INTRADEF.GOUV.FR>
  • References: <E453609450422C4F8EB7A1BA1806686010070EE0@INF31BRUZ--WM15.DR-RES.INTRADEF.GOUV.FR>
Dear all,



I have a question about performing a value analysis on a code that uses a MIN macro.



Here is a piece of code with 3 similar functions.



=======================================================



#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);

   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;

}



=======================================================



The point is that the call to function test2 ends-up with a out-of-bound warning while it is not the case for test1 and test3.



My understanding is that the normalized code should look something like



if ( a < b )

   bound = a;

else

   bound = b;



In the case of test1 the analysis easily remembers that 'a' is less than 'b' if we are in the first branch of the if statement and then is able to bound the variable 'bound' by 10.

In the case of test2 however, the use of binary operands makes it harder to follow. There are two issues here:

                1/ improving value's management of binary operands

                2/ providing to value some information from the source code that is not yet available after pre-processing.

I am not interested in 1/ for this particular question and I would like to adress the point 2/.



As shown by test3, if we use a temporary variable to "force" value to remember that a&0xff is at most 255 and then use atemp in the macro, no more warnings are output.

Naively, we would like to say to value that the source code was issued from a macro and thus if a property of 'a' is true in the condition it is also in the first branch.

Obviously it is not as simple as it sounds if we start thinking about the general case and all the weird things that could be put in a macro still being compliant with the standard.



My question is the following : is this problem potentially solvable (by frama-c developers or may be using ACSL) 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)?



Regards,

Benoît



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20151015/d83a0fce/attachment.html>