--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on May 2011 ---
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