From f3890eb5bdd2d9ae24b3420bd56a1c8d638b9a4e Mon Sep 17 00:00:00 2001 From: Nadrieril <nadrieril+git@gmail.com> Date: Fri, 19 Apr 2024 10:06:06 +0200 Subject: [PATCH] Address review --- charon/src/transform/remove_read_discriminant.rs | 5 +++-- charon/src/values_utils.rs | 1 + 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/charon/src/transform/remove_read_discriminant.rs b/charon/src/transform/remove_read_discriminant.rs index f42b25daf..8601daa48 100644 --- a/charon/src/transform/remove_read_discriminant.rs +++ b/charon/src/transform/remove_read_discriminant.rs @@ -140,8 +140,9 @@ impl<'a, 'tcx, 'ctx> Visitor<'a, 'tcx, 'ctx> { }; } Err(st2) => { - // The discriminant read is not followed by a `SwitchInt`. We replace `_x = - // Discr(_y)` with `match _y { 0 => { _x = 0 }, 1 => { _x = 1; }, .. }`. + // The discriminant read is not followed by a `SwitchInt`. This can happen + // in optimized MIR. We replace `_x = Discr(_y)` with `match _y { 0 => { _x + // = 0 }, 1 => { _x = 1; }, .. }`. let targets = variants .iter_indexed_values() .map(|(id, variant)| { diff --git a/charon/src/values_utils.rs b/charon/src/values_utils.rs index b7aa8e06f..1bdde1105 100644 --- a/charon/src/values_utils.rs +++ b/charon/src/values_utils.rs @@ -218,6 +218,7 @@ impl ScalarValue { ScalarValue::I128(v) => v as u128, } } + pub fn from_bits(ty: IntegerTy, bits: u128) -> Self { Self::from_le_bytes(ty, bits.to_le_bytes()) }