Project Verification 2024 Project 1 Template

This is a Rust re-implementation of the template given for Program Verification.

Correctness

The lexer and parser have been tested a bit and should be roughly correct. In general, I have tried to perfectly match the syntax accepted by the lexer and parser. Since this syntax can be cumbersome to work with, there is also a mode that disables some of the weirdness in the original template like having EParens (which we do not need since we do proper LR parsing). There are some tests for parser and evaluator compatibility, see the python-tests directory.

The Viper AST printer is untested and might print incorrect ASTs. Please double-check your output, and report errors if something breaks.

Relaxed Compatibility Mode

By disabling the syntax-quirks mode, the AST becomes somewhat simplified. You might want to enable this.