Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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