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
Viper Encoding
This chapter details how particular features of the Rust language are encoded into Viper.
Types
Heap-based type encoding
Snapshot-based type encoding
Pure function encoding
Name mangling