Skip to content

Commit

Permalink
Upgrade toolchain to nightly-2024-03-15 (rust-lang#3084)
Browse files Browse the repository at this point in the history
Note that with this upgrade Kani can no longer automatically detect loop bounds when using range.

For more details, see: model-checking/kani#3088
  • Loading branch information
celinval authored Mar 18, 2024
1 parent f54b956 commit 54786ad
Show file tree
Hide file tree
Showing 6 changed files with 6 additions and 2 deletions.
1 change: 1 addition & 0 deletions docs/src/getting-started/verification-results/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
// SPDX-License-Identifier: Apache-2.0 OR MIT

#[kani::proof]
#[kani::unwind(4)]
// ANCHOR: success_example
fn success_example() {
let mut sum = 0;
Expand Down
2 changes: 1 addition & 1 deletion rust-toolchain.toml
Original file line number Diff line number Diff line change
Expand Up @@ -2,5 +2,5 @@
# SPDX-License-Identifier: Apache-2.0 OR MIT

[toolchain]
channel = "nightly-2024-03-14"
channel = "nightly-2024-03-15"
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
2 changes: 1 addition & 1 deletion tests/coverage/unreachable/abort/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
use std::process;

#[kani::proof]
#[cfg_attr(kani, kani::proof, kani::unwind(5))]
fn main() {
for i in 0..4 {
if i == 1 {
Expand Down
1 change: 1 addition & 0 deletions tests/expected/abort/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@
use std::process;

#[kani::proof]
#[kani::unwind(5)]
fn main() {
for i in 0..4 {
if i == 1 {
Expand Down
1 change: 1 addition & 0 deletions tests/expected/iterator/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
// SPDX-License-Identifier: Apache-2.0 OR MIT

#[kani::proof]
#[kani::unwind(4)]
fn main() {
let mut z = 1;
for i in 1..4 {
Expand Down
1 change: 1 addition & 0 deletions tests/kani/Coroutines/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ use std::ops::{Coroutine, CoroutineState};
use std::pin::Pin;

#[kani::proof]
#[kani::unwind(3)]
fn main() {
let mut add_one = |mut resume: u8| {
loop {
Expand Down

0 comments on commit 54786ad

Please sign in to comment.