Code with returns inside conditionals, with code following, doesn't verify properly

An if statement with a return statement inside it doesn't verify properly. The expected behavior is that all code after the if statement should be able to assume the branch with the return statement was not taken. The actual behavior is that a return statement compiles to a variable assignment and then the program doesn't actually return from there, it continues executing until the end of the function. This will cause code after the if statement to execute, and likely break.

I've attached a test case avl-bug3.c0.txt; the assertion //@ assert acc(N->left); on line 38 fails because the verifier thinks that N might be NULL, but that's impossible because in that case the function would already have returned.

This one is easy to work around when writing new short code examples with simple logic, but will be a pain in the neck when scaling up or trying to verify existing codebases.

gradual-verification / gvc0

Code with returns inside conditionals, with code following, doesn't verify properly #32