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



> 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:

You seem to use the definition for "path-sensitive" where only feasible program
paths should be followed.

Consider the following program that manipulates
"arbitrary precision" positive integers:

accept positive integer i
loop with k from 2 to 2*i
  is k prime?
    is 2*i-k prime?
      X=1
      go to L
end loop
X=2
L:
print (X)

According to your definition, any analysis that claims
to be path-sensitive should tell whether X can be
sometimes 1 and sometimes 2, or only possibly 1.
Try self-described "path-sensitive" analysis that you
find in the literature, and tell me it you can get it to conclude.
There is a Fields medal I would like to claim for thinking
of writing this clever program:
http://en.wikipedia.org/wiki/Goldbach%27s_conjecture

Actually, Frama-C provides the closest thing you can
get to a path-sensitive analysis according to your definition
(warning: your definition is not the widely accepted definition).
It provides analyses where you get a first-order logic formula
equivalent to the reachability of point L with X=2.
It is then your job to determine whether that formula is
satisfiable or not. You won't get that Fields medal so easily.

This brings me to another point: as David pointed out,
you shouldn't attribute to Frama-C properties that are only
true of some plug-ins, and false of others.
It gets very irritating over the long run.

Pascal