Skip to content

Commit

Permalink
codegen_scalar: support tuples with more than one element
Browse files Browse the repository at this point in the history
With toolchain versions from 2023-02-05 onwards we have multi-element
tuples in a Scalar (seen for the `(DropMe, Yielded(()))` tuple of
tests/kani/Generator/rustc-generator-tests/smoke-resume-args.rs).
  • Loading branch information
tautschnig committed Apr 13, 2023
1 parent 868b13b commit 33ee94a
Showing 1 changed file with 8 additions and 9 deletions.
17 changes: 8 additions & 9 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
Original file line number Diff line number Diff line change
Expand Up @@ -394,15 +394,14 @@ impl<'tcx> GotocCtx<'tcx> {
}
}
}
(s, ty::Tuple(substs)) => {
// here we have tuples of at most one length
if substs.len() == 1 {
let overall_t = self.codegen_ty(ty);
let t = substs[0];
self.codegen_single_variant_single_field(s, span, overall_t, t)
} else {
unreachable!()
}
(Scalar::Int(int), ty::Tuple(_)) => {
let int_u128 = int.try_to_uint(int.size()).ok().unwrap();
let overall_t = self.codegen_ty(ty);
let expr_int = Expr::int_constant(
int_u128,
Type::unsigned_int(overall_t.sizeof_in_bits(&self.symbol_table)),
);
expr_int.transmute_to(overall_t, &self.symbol_table)
}
(_, ty::Array(_, _)) => {
// we must have zero size array here
Expand Down

0 comments on commit 33ee94a

Please sign in to comment.