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
Types
This section describes how Rust types are encoded into Viper. There are two methods used in Prusti:
Heap-based encoding
Snapshot-based encoding