Support for new expression asserting a in e

[marcoeilers]

Adds support for evaluating the new expression type asserting (a) in e added in viperproject/silver#814.

Based on @dewert99's implementation in PR #455, but instead of killing the branch the assertion is checked in, this PR does it in the same branch. The reasoning behind that change is that one can use the assertion in an asserting expression to create triggering terms that will then be around when evaluating the expression.

[gauravpartha]

Thanks for the PR.

A question on asserting A in e in specifications:

method m(x: Int)
  requires asserting x > 0 in true
  ensures true

Since the precondition is not well-defined according to the current PR is it intended that Viper returns a "specification is not well-formed" error here?

[viper-admin]

Yes, I think that's what you should get. I think it should be analogous to when you have an unfolding in a spec but might not have the predicate.
(Though you need to put parentheses around the x > 0).

[gauravpartha]

Looks good to me.

The only thing that one might want to change is to potentially rename definednessStateOpt in methods of DefinednessComponent (which represents the state in which permissions to reads of heap locations and predicates for unfoldings should be checked during an exhale). The reason is that with asserting A in e it's even more obvious that there are different states in which one performs definedness checks.