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/InterpreterExpressions.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'compiler/InterpreterExpressions.ml')

diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 2223897c..56c0ab5f 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -816,6 +816,7 @@ let eval_rvalue_not_global (config : config) (span : Meta.span)
         "Unreachable: discriminant reads should have been eliminated from the \
          AST"
   | Global _ -> craise __FILE__ __LINE__ span "Unreachable"
+  | Len _ -> craise __FILE__ __LINE__ span "Unhandled Len"
 
 let eval_fake_read (config : config) (span : Meta.span) (p : place) : cm_fun =
  fun ctx ->
-- 
cgit v1.2.3