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

> 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