fixes

.github/workflows/pages.yml

@@ -72,8 +72,6 @@ jobs:
           python x.py doc --all --no-deps
           cp -r ./target/doc ../output/doc
 
-      - name: 
-
       # Only deploy on push to master
       - name: Publish to GitHub pages
         uses: peaceiris/actions-gh-pages@v3

docs/user-guide/src/tour/getting-started.md

@@ -43,7 +43,7 @@ an explicit runtime error, such as
 [`unimplemented!`](https://doc.rust-lang.org/std/macro.unimplemented.html),
 [`todo!`](https://doc.rust-lang.org/std/macro.todo.html), or
 possibly a failing [assertion](https://doc.rust-lang.org/std/macro.assert.html),
-is reachable. [Prusti assertions](../verify/assert_assume.md) are also checked. These are like the normal `assert!` statements, but they can use the full Prusti specification syntax and will not result in any runtime checks or code when compiled normally.
+is reachable. [Prusti assertions](../verify/assert_refute_assume.md) are also checked. These are like the normal `assert!` statements, but they can use the full Prusti specification syntax and will not result in any runtime checks or code when compiled normally.
 
 For example, the following test function creates a node with no successor and panics
 if the node's payload is greater than 23:

docs/user-guide/src/tour/new.md

@@ -102,10 +102,12 @@ error: [Prusti: invalid specification] use of impure function "Link::len" in pur
 
 Whenever we add the attribute `#[pure]` to a function, Prusti will check whether that
 function is indeed deterministic and side-effect free
-(notice that [termination](../capabilities/limitations.md#termination-checks-total-correctness-missing) is *not* checked); otherwise, it complains.
+(notice that termination is *not* checked); otherwise, it complains.
 In this case, Prusti complains because we call an impure function,
 namely `Link::len()`, within the body of the pure function `List::len()`.
 
+<!-- TODO: link capabilities/limitations chapter (termination) -->
+
 To fix this issue, it suffices to mark `Link::len()` as pure as well.
 
 ```rust,noplaypen

docs/user-guide/src/tour/option.md

@@ -22,7 +22,9 @@ Changing the `Link` type requires some adjustments of the code and specification
 {{#rustdoc_include ../../../../prusti-tests/tests/verify/pass/user-guide/option.rs:rewrite_link_impl}}
 ```
 
-Due to current [limitations of Prusti](../capabilities/limitations.md#loops-in-pure-functions-unsupported), we cannot replace our `link_len` and `link_lookup` functions with loops:
+Due to current limitations of Prusti, we cannot replace our `link_len` and `link_lookup` functions with loops:
+
+<!-- TODO: link capabilities/limitations chapter (loops in pure functions) -->
 
 ```rust,noplaypen,ignore
 {{#rustdoc_include ../../../../prusti-tests/tests/verify/fail/user-guide/option_loops_in_pure_fn.rs:code}}

docs/user-guide/src/tour/peek.md

@@ -3,7 +3,9 @@
 > **Recommended reading:** 
 > [3.3: Peek](https://rust-unofficial.github.io/too-many-lists/second-peek.html)
 
-Ideally, we could implement `peek` and `try_peek` like we implemented `pop` and `try_pop` before. Like `pop`, `push` can only be called if the list is non-empty, and it then always returns a reference to the element at the head of the list (type `&T`). Similarly, `try_peek` can be called on any list, but returns an `Option<&T>`. The latter is currently not possible in Prusti, since structures containing references are not supported at the moment (see chapter [Prusti Limitations](../capabilities/limitations.md)).
+Ideally, we could implement `peek` and `try_peek` like we implemented `pop` and `try_pop` before. Like `pop`, `push` can only be called if the list is non-empty, and it then always returns a reference to the element at the head of the list (type `&T`). Similarly, `try_peek` can be called on any list, but returns an `Option<&T>`. The latter is currently not possible in Prusti, since structures containing references are not supported at the moment.
+
+<!-- TODO: link capabilities/limitations chapter (refs in structs) -->
 
 We can still implement `peek`, but we just cannot do it by using `try_peek` like before in `pop`. Instead, we can reuse the already implemented and verified `lookup` function! Since `lookup` can return a reference to any element of the list, we can just call `self.lookup(0)` inside of `peek`: 
 

docs/user-guide/src/tour/pledges.md

@@ -9,7 +9,9 @@ We will demonstrate by implementing a function that gives you a mutable referenc
 The `peek_mut` will return a mutable reference of type `T`, so the precondition of the list requires it to be non-empty.
 As a first postcondition, we want to ensure that the `result` of `peek_mut` points to the first element of the list.
 
-In the code, we need to get a mutable reference to the type inside the `Link = Option<Box<Node<T>>>`. This requires the use of the type `Option<&mut T>`, which is a structure containing a reference, so it is not yet supported by Prusti (see [limitations chapter](../capabilities/limitations.md)). To still be able to verify `peek_mut`, we mark it as `trusted` for now:
+In the code, we need to get a mutable reference to the type inside the `Link = Option<Box<Node<T>>>`. This requires the use of the type `Option<&mut T>`, which is a structure containing a reference, so it is not yet supported by Prusti. To still be able to verify `peek_mut`, we mark it as `trusted` for now:
+
+<!-- TODO: link capabilities/limitations chapter (refs in structs) -->
 
 ```rust,noplaypen
 {{#rustdoc_include ../../../../prusti-tests/tests/verify/fail/user-guide/peek_mut_pledges.rs:peek_mut_code}}

docs/user-guide/src/tour/setup.md

@@ -33,8 +33,9 @@ In this file, you can set [configuration flags](https://viperproject.github.io/p
 check_overflows = false
 ```
 
-**Note**: Creating a new project will create a `main.rs` file containing a `Hello World` program. Since Prusti does not yet support Strings (see [Prusti Limitations](../capabilities/limitations.md#strings-and-string-slices) chapter), verification will fail on `main.rs`. To still verify the code, remove the line `println!("Hello, world!");`.
+**Note**: Creating a new project will create a `main.rs` file containing a `Hello World` program. Since Prusti does not yet support Strings, verification will fail on `main.rs`. To still verify the code, remove the line `println!("Hello, world!");`.
 
+<!-- TODO: link capabilities/limitations chapter (strings) -->
 
 ## Standard library annotations
 

docs/user-guide/src/verify/assert_refute_assume.md

@@ -10,6 +10,8 @@ function (via an assumption).
 The macros `prusti_assert!`, `prusti_assert_eq!` and `prusti_assert_ne!` instruct Prusti to verify that a certain property holds at a specific point within the body of a function. In contrast to the `assert!`, `assert_eq!` and `assert_ne!` macros, which only accept Rust expressions, the Prusti variants accept [specification](../syntax.md) expressions as arguments. Therefore, [quantifiers](../syntax.md#quantifiers), [`old`](../syntax.md#old-expressions) expressions and other Prusti specification syntax is allowed within a call to `prusti_assert!`, as in the following example:
 
 ```rust,noplaypen,ignore
+# // The next line is only required for doctests, you can ignore/remove it
+# extern crate prusti_contracts;
 # use prusti_contracts::*;
 # 
 #[requires(*x != 2)]
@@ -22,6 +24,8 @@ fn go(x: &mut u32) {
 The two macros `prusti_assert_eq!` and `prusti_assert_ne!` are also slightly different than their standard counterparts, in that they use [snapshot equality](../syntax.md#snapshot-equality) `===` instead of [Partial Equality](https://doc.rust-lang.org/std/cmp/trait.PartialEq.html) `==`.
 
 ```rust,noplaypen,ignore
+# // The next line is only required for doctests, you can ignore/remove it
+# extern crate prusti_contracts;
 # use prusti_contracts::*;
 # 
 #[requires(a === b)]
@@ -42,6 +46,8 @@ fn different(a: u64, b: u64) {
 Note that the expression given to `prusti_assert!` must be side-effect free, since they will not result in any runtime code. Therefore, using code containing [impure](../verify/pure.md) functions will work in an `assert!`, but not within a `prusti_assert!`. For example:
 
 ```rust,noplaypen,ignore
+# // The next line is only required for doctests, you can ignore/remove it
+# extern crate prusti_contracts;
 # use prusti_contracts::*;
 # 
 # fn test(map: std::collections::HashMap) {
@@ -59,6 +65,10 @@ Using Prusti assertions instead of normal assertions can speed up verification,
 The `prusti_refute!` macro is similar to `prusti_assert!` in its format, conditions of use and what expressions it accepts. It instructs Prusti to verify that a certain property at a specific point within the body of a function might hold in some, but not all cases. For example the following code will verify:
 
 ```rust,noplaypen
+# // The next line is only required for doctests, you can ignore/remove it
+# extern crate prusti_contracts;
+# use prusti_contracts::*;
+# 
 #[ensures(val < 0 ==> result == -1)]
 #[ensures(val == 0 ==> result == 0)]
 #[ensures(val > 0 ==> result == 1)]
@@ -78,7 +88,11 @@ fn sign(val: i32) -> i32 {
 
 But the following function would not:
 
-```rust,noplaypen
+```rust,noplaypen,ignore
+# // The next line is only required for doctests, you can ignore/remove it
+# extern crate prusti_contracts;
+# use prusti_contracts::*;
+# 
 #[requires(val < 0 && val > 0)]
 #[ensures(result == val/2)]
 fn half(val: i32) -> i32 {
@@ -95,6 +109,10 @@ this can be used to introduce unsoundness. For example, Prusti would verify the
 following function:
 
 ```rust,noplaypen,ignore
+# // The next line is only required for doctests, you can ignore/remove it
+# extern crate prusti_contracts;
+# use prusti_contracts::*;
+# 
 #[ensures(p == np)]
 fn proof(p: u32, np: u32) {
     prusti_assume!(false);

prusti-contracts/prusti-contracts-proc-macros/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "prusti-contracts-proc-macros"
-version = "0.1.6"
+version = "0.1.8"
 authors = ["Prusti Devs <[email protected]>"]
 edition = "2021"
 license = "MPL-2.0"
@@ -15,7 +15,7 @@ categories = ["development-tools", "development-tools::testing"]
 proc-macro = true
 
 [dependencies]
-prusti-specs = { path = "../prusti-specs", version = "0.1.6", optional = true }
+prusti-specs = { path = "../prusti-specs", version = "0.1.8", optional = true }
 proc-macro2 = { version = "1.0", optional = true }
 
 [features]

prusti-contracts/prusti-contracts/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "prusti-contracts"
-version = "0.1.6"
+version = "0.1.8"
 authors = ["Prusti Devs <[email protected]>"]
 edition = "2021"
 license = "MPL-2.0"
@@ -12,7 +12,7 @@ keywords = ["prusti", "contracts", "verification", "formal", "specifications"]
 categories = ["development-tools", "development-tools::testing"]
 
 [dependencies]
-prusti-contracts-proc-macros = { path = "../prusti-contracts-proc-macros", version = "0.1.6" }
+prusti-contracts-proc-macros = { path = "../prusti-contracts-proc-macros", version = "0.1.8" }
 
 [dev-dependencies]
 trybuild = "1.0"

prusti-contracts/prusti-specs/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "prusti-specs"
-version = "0.1.7"
+version = "0.1.8"
 authors = ["Prusti Devs <[email protected]>"]
 edition = "2021"
 license = "MPL-2.0"

prusti-contracts/prusti-std/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "prusti-std"
-version = "0.1.6"
+version = "0.1.8"
 authors = ["Prusti Devs <[email protected]>"]
 edition = "2021"
 license = "MPL-2.0"
@@ -12,7 +12,7 @@ keywords = ["prusti", "contracts", "verification", "formal", "specifications"]
 categories = ["development-tools", "development-tools::testing"]
 
 [dependencies]
-prusti-contracts = { path = "../prusti-contracts", version = "0.1.6" }
+prusti-contracts = { path = "../prusti-contracts", version = "0.1.8" }
 
 # Forward "prusti" flag
 [features]