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



Hi,

I'm just wondering if Frama C's analyses are path-sensitive or not. 
Consider the following program:

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?

Thank you!

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