Turn Aeneas into a borrow checker

[sonmarcho]

trafficstars

We could turn Aeneas into a borrow checker by printing informative error messages when there is a borrow checking error (or more generally speaking an invalid access, in particular to a bottom value), and not aborting on the first error.

This issue should be solved after https://github.com/AeneasVerif/aeneas/issues/54.