diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 01dacb3b10d5..8d212c75fda4 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -331,7 +331,6 @@ impl<'tcx> GotocCtx<'tcx> { }; let overall_t = self.codegen_ty(ty); let direct_fields = overall_t.lookup_field("direct_fields", &self.symbol_table).unwrap(); - let mut operands_iter = operands.iter(); let direct_fields_expr = Expr::struct_expr_from_values( direct_fields.typ(), layout @@ -342,13 +341,12 @@ impl<'tcx> GotocCtx<'tcx> { if idx == *discriminant_field { Expr::int_constant(0, self.codegen_ty(field_ty)) } else { - self.codegen_operand(operands_iter.next().unwrap()) + self.codegen_operand(&operands[idx]) } }) .collect(), &self.symbol_table, ); - assert!(operands_iter.next().is_none()); Expr::union_expr(overall_t, "direct_fields", direct_fields_expr, &self.symbol_table) } diff --git a/tests/kani/Generator/issue-2434.rs b/tests/kani/Generator/issue-2434.rs new file mode 100644 index 000000000000..fd84ccfa197a --- /dev/null +++ b/tests/kani/Generator/issue-2434.rs @@ -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 + Sync + 'static>>; + +pub struct Scheduler { + task: Option, +} + +impl Scheduler { + /// Adds a future to the scheduler's task list, returning a JoinHandle + pub fn spawn + 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 + 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; + } + }; + }); +}