--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on May 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama C path sensitiveness



Thanks for the quick reply sir!

In that program you were able to solve the problem by assigning a 
temporary variable because the expressions were the same. But the 
following program still does not work:

extern int n1, n2;
main() {
     int a = 0, b,t1,t2;

     t1 = n1 > n2;
     t2 = n1 == n2+1;

     if(t1) { a = 4; }
     else if(t2) { a = 5; }

     b = a+1;
     return b;
}

Even here a = 5 is dead code since t2 implies t1, but the value analysis 
plugin is not able to catch it. Can you explain how this happens?

Thank you!

------
Vijayaraghavan Murali
http://www.comp.nus.edu.sg/~mvijayar


On 23/05/2011 15:29, David MENTRE wrote:
> Hello Mr Mural,
>
> 2011/5/23 Vijayaraghavan Murali<m.vijay at nus.edu.sg>:
>> I'm just wondering if Frama C's analyses are path-sensitive or not. Consider
>> the following program:
>
> You mean: "is value analysis *plugin* or Frama-C framework is path senstitive?"
>
> Yes.
>
>> extern int n1,n2;
>> int main() {
>>      int a = 0, b;
>>
>>      if(n1<  n2) { a = 4; }
>>      else if(n1<  n2) { a = 5; }
>>
>>      b = a+1;
>>      return b;
>> }
>>
>> Clearly the 2nd branch is infeasible, so a = 5 is essentially dead code. But
>> the domain of 'a' is reported to be {0, 4, 5} and use-def analysis on the
>> assignment to 'b' returns {a = 0; a = 4; a = 5;}. From this it looks like
>> Frama C is not path-sensitive. Can someone explain?
>
> It seems that the "n1<  n2" expression is a bit too complicated for
> the value analysis plugin. The following equivalent program shows the
> result you were expecting (second assignment is dead code, a ? {0; 4;
> }):
>
> """
> extern int n1,n2;
>
> int main() {
>    int a = 0, b, t;
>
>      t = n1<  n2;
>      if(t) { a = 4; }
>      else if(t) { a = 5; }
>
>      b = a+1;
>      return b;
> }
> """
>
> Analysed with:
>    frama-c -val -slevel 4 murali.c
>
> frama-c -version
> Version: Boron-20100401
>
> Value analysis plugin author will probably comment on the differences
> between the two programs. I tried to add an "//@ assert n1<  n2 || n1
>> = n2;" before the first if to help the analysis without much success.
>
> Sincerely yours,
> david