Re: [abc] PLDI paper

> 8) Damien mentioned a variation of our inter-proc algorithm ... Damien ...
> what was it - something about not needed something on "all paths"?

I just noticed in chicago that the condition for setting a cflow
residue to alwaysMatch is stronger than it needs to be -

  what i would expect would be
a query shadow qsh is statically true if for every interprocedural
path p to qsh there is an update shadow in p
[where an interprocedural path includes calls but not returns]

whereas the condition that there is an update shadow sh such that qsh
is in mustCflow(sh) is equivalent to :
every interprocedural path p to qsh goes through sh [ie all paths must
go through the same shadow]

(please check that i haven't made some mistake along the way!)

I guess the mustCflow version is probably easier / more efficient to
compute, but maybe we should mention the other one (of course, the
benchmarks show the mustCflow is precise enough)

Cheers,
Damien
Received on Sat Apr 9 19:35:37 2005