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
Development
Setup
Building
Tests
IDE integration
Debugging