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