Assert and Unfold in pure functions

[marcoeilers]

This PR adds the ability to use Unfold(P(...)) and Assert(e) as statements inside pure functions the same way they can be used in non-pure functions: Assert checks if the given assertion holds at this point in the program, and Unfold unfolds the given predicate on the given path (s.t. it remains unfolded on this path).

They are translated into unfolding and asserting expressions on the Viper level.

---

This change is