limit check insertion

[Henry Cejtin]

I assume that the last defining case of V should have been
    V (l :: p, n) = V (p, n - m) if at(l) = Alloc(m)
                                 if at(l) = LimitCheck(m)
I.e.,  you  have to walk through the path, not just take the first element of
the path, and what you called `li' was just `l'.  (Is the  first  part  wrong
because all allocations and checks are at the start of a basic block?)

Isn't  it  incorrect  (needlessly  resrictive)  to  allow paths to start from
arbitrary positions?  I.e., if I have some code that does a limit  check  and
then  goes to another block which does some allocation, then I am safe, but I
would fail your requirements since the path which starts  at  the  allocation
would have a V which was negative.