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