Tests

Tests for the Prusti project can be executed using the Python wrapper script:

./x.py test

The script sets up environment variables just like in the build phase, then runs cargo test.

Any additional arguments are added to the cargo test command line. For example:

$ ./x.py test --all --verbose

Filtering tests

The options available when running cargo test still apply. For example, to only run tests which contain mod in their name:

$ ./x.py test mod

Additional flags

Some tests require setting additional flags, for example, to ensure that the number of quantifier instantiations is below a certain bound. This can be achieved by adding at the top of the test file // compile-flags: followed by the list of arguments to Prusti. For example, the following comment would bound the number of unique triggers used to instantiate a quantifier to 20:

#![allow(unused)]
fn main() {
// compile-flags: -Psmt_unique_triggers_bound=20
}

Debugging tests

See the debugging section.