Assume now accepts impure assertions

[viper-admin]

Created by @fabiopakk on 2019-06-20 12:44

https://github.com/viperproject/tutorial/issues/162 states that assume is being translated to inhale and is therefore inadvertently allowing impure assertions to be used with assume. As the discussion in https://github.com/viperproject/tutorial/issues/162 shows, this description is outdated and impure assertions are now supported in assume. However the Viper tutorial still states the opposite.

When fixing this part of the tutorial, please refer to https://github.com/viperproject/tutorial/issues/162 in Silver for further references to the work that implemented such extension.

[Aurel300]

@alexanderjsummers Can you comment on the resolution here? The linked discussion is a bit confusing. The tutorial currently states (wrongly):

• assume E is equivalent to inhale E; note that it takes an expression rather than an assertion, which must not contain resource assertions such as accessibility predicates; this restriction may be lifted in future versions of Viper.

I think even saying "is equivalent to" is wrong, because assume acc(...) is different from inhale acc(...), right?