Framing runtime checks should be emitted at the end of each loop iteration

[hgouni]

This can be seen in the loop_something.c0 example. We begin the append method with no permissions, and in an imprecise state. When we encounter the while loop on line 20, we correctly emit a check for asserting that we have access to n->next. The first iteration of the loop is fine, because we have checked that we have access to n->next. Before we begin the next iteration, though, we should check again that we have access to n->next (since we might've lost it on the current iteration). If we don't have access, the program shouldn't be able to evaluate the loop condition, and should crash. This currently isn't done, which results in a soundness issue.

[hgouni]

A potential further issue is that the check for before the loop body isn't annotated with the correct loop position type, but instead is mapped directly from the AST node for the field access in the loop condition (or it looks like that). This may be acceptable behavior, but I'm not sure yet.