limit check insertion

[Stephen Weeks]

> 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?)

Sorry, the definition should have been

Definition [V]:
   V: Path x Int -> Int
   V ([], n) = n
   V (l :: p, n) = V(p, n - m)  if at(l) = Alloc(m)
		   V(p, m)      if at(l) = LimitCheck(m)

This framework abstracts away from basic blocks, which can be
represented as statements with only one successor.
 
> Isn't  it  incorrect  (needlessly  resrictive)  to  allow paths to start from
> arbitrary positions?

Yes.  That is why, the definitions of soundness and correctness only
refered to paths starting at ls.