Skip to content

Commit

Permalink
Update Prusti Dev Guide - links to a wrong file (viperproject#1293)
Browse files Browse the repository at this point in the history
The [prusti dev guide - 3. Verification Pipeline, 3.2. Rust compilation stage](https://viperproject.github.io/prusti-dev/dev-guide/pipeline/rust.html) refers to [prusti-dev/prusti/src/lib.rs](https://github.com/viperproject/prusti-dev/blob/9ca9cd1b9bcfd9870691fa5a7a957a90987ba4af/prusti/src/lib.rs#L44), however, this mentioned code/functions have been moved to [prusti-dev/prusti/src/lib.rs](https://github.com/viperproject/prusti-dev/blob/f6850c5036c4a85c8812b46eed8ac472ca95fe25/prusti/src/callbacks.rs#L58).
  • Loading branch information
simon-hrabec committed Jan 27, 2023
1 parent 706512a commit 17b071c
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions docs/dev-guide/src/pipeline/rust.md
Original file line number Diff line number Diff line change
Expand Up @@ -7,5 +7,5 @@

In this stage, the actual Rust compiler is invoked to make sure the given code is valid Rust code, both syntactically and semantically. Prusti integrates with the Rust compiler using [`rustc_driver`](https://rustc-dev-guide.rust-lang.org/rustc-driver.html). This allows running the Rust compiler with [callbacks](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_driver/trait.Callbacks.html) triggered when important stages of processing are completed. In Prusti, we are interested in two stages:

- [`prusti/src/lib.rs` - `PrustiCompilerCalls::after_expansion`](https://github.com/viperproject/prusti-dev/blob/9ca9cd1b9bcfd9870691fa5a7a957a90987ba4af/prusti/src/lib.rs#L44) - for debugging and unit testing purposes, it is useful to see the Rust AST after the Prusti specifications are processed.
- [`prusti/src/lib.rs` - `PrustiCompilerCalls::after_analysis`](https://github.com/viperproject/prusti-dev/blob/9ca9cd1b9bcfd9870691fa5a7a957a90987ba4af/prusti/src/lib.rs#L64) - once the type checking is done and the code is determined to be type safe. Code that is syntactically invalid or has type errors is not relevant for Prusti applications.
- [`prusti/src/callbacks.rs` - `PrustiCompilerCalls::after_expansion`](https://github.com/viperproject/prusti-dev/blob/f6850c5036c4a85c8812b46eed8ac472ca95fe25/prusti/src/callbacks.rs#L58) - for debugging and unit testing purposes, it is useful to see the Rust AST after the Prusti specifications are processed.
- [`prusti/src/callbacks.rs` - `PrustiCompilerCalls::after_analysis`](https://github.com/viperproject/prusti-dev/blob/f6850c5036c4a85c8812b46eed8ac472ca95fe25/prusti/src/callbacks.rs#L89) - once the type checking is done and the code is determined to be type safe. Code that is syntactically invalid or has type errors is not relevant for Prusti applications.

0 comments on commit 17b071c

Please sign in to comment.