-
Notifications
You must be signed in to change notification settings - Fork 97
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Fix the order of operands for generator structs (#2436)
- Loading branch information
1 parent
708bc35
commit c3d28e0
Showing
2 changed files
with
54 additions
and
3 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,53 @@ | ||
// Copyright Kani Contributors | ||
// SPDX-License-Identifier: Apache-2.0 OR MIT | ||
// | ||
// compile-flags: --edition 2018 | ||
|
||
//! Regression test for https://github.com/model-checking/kani/issues/2434 | ||
//! The problem was an incorrect order for the operands | ||
use core::{future::Future, pin::Pin}; | ||
|
||
type BoxFuture = Pin<Box<dyn Future<Output = ()> + Sync + 'static>>; | ||
|
||
pub struct Scheduler { | ||
task: Option<BoxFuture>, | ||
} | ||
|
||
impl Scheduler { | ||
/// Adds a future to the scheduler's task list, returning a JoinHandle | ||
pub fn spawn<F: Future<Output = ()> + Sync + 'static>(&mut self, fut: F) { | ||
self.task = Some(Box::pin(fut)); | ||
} | ||
} | ||
|
||
/// Polls the given future and the tasks it may spawn until all of them complete | ||
/// | ||
/// Contrary to block_on, this allows `spawn`ing other futures | ||
pub fn spawnable_block_on<F: Future<Output = ()> + Sync + 'static>( | ||
scheduler: &mut Scheduler, | ||
fut: F, | ||
) { | ||
scheduler.spawn(fut); | ||
} | ||
|
||
/// Sender of a channel. | ||
pub struct Sender {} | ||
|
||
impl Sender { | ||
pub async fn send(&self) {} | ||
} | ||
|
||
#[kani::proof] | ||
fn check() { | ||
let mut scheduler = Scheduler { task: None }; | ||
spawnable_block_on(&mut scheduler, async { | ||
let num: usize = 1; | ||
let tx = Sender {}; | ||
|
||
let _task1 = async move { | ||
for _i in 0..num { | ||
tx.send().await; | ||
} | ||
}; | ||
}); | ||
} |