From 1e56d816cb386747b2155a77f7b396f6f9e79517 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 30 Jul 2025 10:26:35 +0000 Subject: [PATCH] Set bits_per_byte in byte_extract expressions CBMC expected the number of bits-in-a-byte to be set as part of a byte_extract expression ever since diffblue/cbmc@a8631c514be3c5, but seemingly produces correct verification results even when CBMC finds that value to be 0 (but might fail to apply certain optimisations). An upcoming change on the CBMC side adds additional sanity checks, which uncovered this omission on Kani's part. --- cprover_bindings/src/irep/to_irep.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index 23d31329eb86..85918ac56633 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/cprover_bindings/src/irep/to_irep.rs @@ -225,7 +225,7 @@ impl ToIrep for ExprValue { IrepId::ByteExtractLittleEndian }, sub: vec![e.to_irep(mm), Expr::int_constant(*offset, Type::ssize_t()).to_irep(mm)], - named_sub: linear_map![], + named_sub: linear_map![(IrepId::BitsPerByte, Irep::just_int_id(8u8))], }, ExprValue::CBoolConstant(i) => Irep { id: IrepId::Constant,