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] 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