From 652e5c12bf34a9dd3be11c23425d3c6500ce8c43 Mon Sep 17 00:00:00 2001
From: Nadrieril <nadrieril+git@gmail.com>
Date: Thu, 20 Feb 2025 17:11:40 +0100
Subject: [PATCH] Update charon

---
 charon-pin                           | 2 +-
 flake.lock                           | 6 +++---
 src/interp/InterpreterExpressions.ml | 8 ++++++--
 3 files changed, 10 insertions(+), 6 deletions(-)

diff --git a/charon-pin b/charon-pin
index 81a6e3fd..1eab898a 100644
--- a/charon-pin
+++ b/charon-pin
@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-5651efc286dcee58e8e96be869980a40a26af95c
+368d17ccff13e3c09d4438c74a1227a0d6f6577e
diff --git a/flake.lock b/flake.lock
index 475ef9e1..e6c3336d 100644
--- a/flake.lock
+++ b/flake.lock
@@ -12,11 +12,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1739392485,
-        "narHash": "sha256-HbSbQHWCvwOGQQBBZx427rBWEpE8zBB/CWdd9+I6Fxk=",
+        "lastModified": 1740066723,
+        "narHash": "sha256-5UApG4QBZWkkITYJ0iwh22ECYeKgYfRq0KeSfdCj8s8=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "5651efc286dcee58e8e96be869980a40a26af95c",
+        "rev": "368d17ccff13e3c09d4438c74a1227a0d6f6577e",
         "type": "github"
       },
       "original": {
diff --git a/src/interp/InterpreterExpressions.ml b/src/interp/InterpreterExpressions.ml
index b5c37de5..a3418224 100644
--- a/src/interp/InterpreterExpressions.ml
+++ b/src/interp/InterpreterExpressions.ml
@@ -373,7 +373,7 @@ let eval_operand_no_reorganize (config : config) (span : Meta.span)
       ^ "\n"));
   (* Evaluate *)
   match op with
-  | Constant cv -> (
+  | Constant cv -> begin
       match cv.value with
       | CLiteral lit -> (
           (* FIXME: the str type is not in [literal_type] *)
@@ -447,7 +447,11 @@ let eval_operand_no_reorganize (config : config) (span : Meta.span)
           (cv, ctx, cc_comp cc cf)
       | CFnPtr _ ->
           craise __FILE__ __LINE__ span
-            "Function pointers are not supported yet")
+            "Function pointers are not supported yet"
+      | CRawMemory _ ->
+          craise __FILE__ __LINE__ span
+            "Raw memory cannot be interpreted by the interpreter"
+    end
   | Copy p ->
       (* Access the value *)
       let access = Read in