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



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