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