Skip to content

Commit 9fcac41

Browse files
authored
Fix slow generator tests by adding kani::unwind annotation (rust-lang#1408)
1 parent c4ddf6c commit 9fcac41

File tree

2 files changed

+7
-10
lines changed

2 files changed

+7
-10
lines changed

tests/kani/Generator/rustc-generator-tests/niche-in-generator-slow_fixme.rs tests/kani/Generator/rustc-generator-tests/niche-in-generator.rs

+3-5
Original file line numberDiff line numberDiff line change
@@ -20,16 +20,14 @@ use std::mem::size_of_val;
2020
fn take<T>(_: T) {}
2121

2222
#[kani::proof]
23+
#[kani::unwind(2)]
2324
fn main() {
2425
let x = false;
2526
let mut gen1 = || {
2627
yield;
2728
take(x);
2829
};
2930

30-
// FIXME: for some reason, these asserts are very hard for CBMC to figure out
31-
// Kani didn't terminate within 5 minutes.
32-
// assert_eq!(Pin::new(&mut gen1).resume(()), GeneratorState::Yielded(()));
33-
// assert_eq!(Pin::new(&mut gen1).resume(()), GeneratorState::Complete(()));
34-
assert!(false); // to make the test fail without taking forever
31+
assert_eq!(Pin::new(&mut gen1).resume(()), GeneratorState::Yielded(()));
32+
assert_eq!(Pin::new(&mut gen1).resume(()), GeneratorState::Complete(()));
3533
}

tests/kani/Generator/rustc-generator-tests/size-moved-locals-slow_fixme.rs tests/kani/Generator/rustc-generator-tests/size-moved-locals.rs

+4-5
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@
2626
use std::ops::{Generator, GeneratorState};
2727
use std::pin::Pin;
2828

29-
const FOO_SIZE: usize = 1024;
29+
const FOO_SIZE: usize = 128;
3030
struct Foo([u8; FOO_SIZE]);
3131

3232
impl Drop for Foo {
@@ -79,9 +79,9 @@ fn overlap_x_and_y() -> impl Generator<Yield = (), Return = ()> {
7979
}
8080

8181
#[kani::proof]
82+
#[kani::unwind(129)]
8283
fn main() {
83-
// FIXME: the following tests are very slow (did not terminate in a couple of minutes)
84-
/* let mut generator = move_before_yield();
84+
let mut generator = move_before_yield();
8585
assert_eq!(
8686
unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
8787
GeneratorState::Yielded(())
@@ -131,6 +131,5 @@ fn main() {
131131
assert_eq!(
132132
unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
133133
GeneratorState::Complete(())
134-
); */
135-
assert!(false); // to make the test fail without taking forever
134+
);
136135
}

0 commit comments

Comments
 (0)