1.
Introduction
2.
Configuration
2.1.
Providing Flags
2.2.
List of Configuration Flags
3.
Verification Pipeline
3.1.
Binary stage
3.2.
Rust compilation stage
3.3.
Prusti processing stage
3.4.
Viper verification stage
3.5.
Reporting stage
4.
Macros
5.
Viper Encoding
5.1.
Types
5.1.1.
Heap-based type encoding
5.1.2.
Snapshot-based type encoding
5.2.
Pure function encoding
5.3.
Name mangling
6.
Repository Layout
7.
Development
7.1.
Setup
7.2.
Building
7.3.
Tests
7.4.
IDE integration
7.5.
Debugging
Light
Rust
Coal
Navy
Ayu
Prusti dev guide
Configuration
Providing Flags
List of Configuration Flags