Merge pull request #443 from Nadrieril/update-charon2

AeneasVerif · Feb 20, 2025 · 2c2514b · 2c2514b
2 parents 29d05d8 + 652e5c1
commit 2c2514b
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 6 deletions.
diff --git 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
diff --git 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