search

viperproject / carbon

Verification-condition-generation-based verifier for the Viper intermediate verification language.
Mozilla Public License 2.0
30 stars 21 forks source link

Support for new expression asserting a in e #531

Closed marcoeilers closed 2 weeks ago

marcoeilers commented 1 month ago

Adds support for evaluating the new expression type asserting (a) in e added in https://github.com/viperproject/silver/pull/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 commented 1 month ago

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 commented 1 month ago

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).