viperproject / silicon

Symbolic-execution-based verifier for the Viper intermediate verification language.
Mozilla Public License 2.0
79 stars 31 forks source link

Support for new assertin expressions #875

Open marcoeilers opened 1 day ago

marcoeilers commented 1 day ago

Adds support for evaluating the new expression type asserting (a) in e added in https://github.com/viperproject/silver/pull/814.