From ec039b63748c2a95f89c0538a843e18d3a51cdf3 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino
Date: Mon, 3 Jun 2024 16:53:09 +0200
Subject: feat: basic handling for `RValue::Len`, following
 AeneasVerif/charon#209

---
 compiler/InterpreterUtils.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'compiler/InterpreterUtils.ml')

diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 653a0e24..f3f12906 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -291,7 +291,7 @@ let rvalue_get_place (rv : rvalue) : place option =
   match rv with
   | Use (Copy p | Move p) -> Some p
   | Use (Constant _) -> None
-  | RvRef (p, _) -> Some p
+  | Len (p, _, _) | RvRef (p, _) -> Some p
   | UnaryOp _ | BinaryOp _ | Global _ | Discriminant _ | Aggregate _ -> None
 
 (** See {!ValuesUtils.symbolic_value_has_borrows} *)
-- 
cgit v1.2.3