From d3f52e23ede39c4fd7845b6c5feb29d28b2a2384 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 21 Jun 2024 15:47:56 +0200
Subject: Update charon
---
charon-pin | 2 +-
compiler/FunsAnalysis.ml | 7 +++++++
compiler/Interpreter.ml | 2 +-
compiler/Print.ml | 1 -
compiler/Translate.ml | 3 +++
flake.lock | 6 +++---
scripts/update-charon-pin.sh | 2 +-
tests/src/mutually-recursive-traits.lean.out | 6 +++---
8 files changed, 19 insertions(+), 10 deletions(-)
diff --git a/charon-pin b/charon-pin
index 838e423c..e4f6e42a 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.
-81c0edf20eefb55a0b2f2bc5ab029ec96e75a82c
+61685783db8135df945e53b302dc3e364b7892ee
diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index 815c470f..e0a86145 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -223,6 +223,13 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
let global = GlobalDeclId.Map.find id globals_map in
analyze_fun_decl_group (NonRecGroup global.body);
analyze_decl_groups decls'
+ | MixedGroup ids :: _ ->
+ craise_opt_span __FILE__ __LINE__ None
+ ("Mixed declaration groups are not supported yet: ["
+ ^ String.concat ", "
+ (List.map Charon.PrintGAst.any_decl_id_to_string
+ (Charon.GAstUtils.g_declaration_group_to_list ids))
+ ^ "]")
in
analyze_decl_groups m.declarations;
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 7e292906..075672fe 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -17,7 +17,7 @@ module SA = SymbolicAst
let log = Logging.interpreter_log
let compute_contexts (m : crate) : decls_ctx =
- let type_decls_list, _, _, _, _ = split_declarations m.declarations in
+ let type_decls_list, _, _, _, _, _ = split_declarations m.declarations in
let type_decls = m.type_decls in
let fun_decls = m.fun_decls in
let global_decls = m.global_decls in
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 76793548..90dadbcc 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -5,7 +5,6 @@ open Charon.PrintTypes
open Charon.PrintExpressions
open Charon.PrintLlbcAst.Ast
open Types
-open TypesUtils
open Values
open ValuesUtils
open Expressions
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 23c0782a..0474d233 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -820,6 +820,9 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
| TraitImplGroup id ->
if config.extract_trait_impls && config.extract_transparent then
export_trait_impl id
+ | MixedGroup _ ->
+ craise_opt_span __FILE__ __LINE__ None
+ "Mixed-recursive declaration groups are not supported"
in
(* If we need to export the state type: we try to export it after we defined
diff --git a/flake.lock b/flake.lock
index 948d25d2..a35ba103 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
"rust-overlay": "rust-overlay"
},
"locked": {
- "lastModified": 1718897879,
- "narHash": "sha256-sRbyKlrsEgx7FYDjlYeQpT8wLUgfBiNnMqEQ5029K14=",
+ "lastModified": 1718979132,
+ "narHash": "sha256-MZbG1JOuKpV47fVfi+OhUsf3uRG+ln2KseMNitxqHmQ=",
"owner": "aeneasverif",
"repo": "charon",
- "rev": "81c0edf20eefb55a0b2f2bc5ab029ec96e75a82c",
+ "rev": "61685783db8135df945e53b302dc3e364b7892ee",
"type": "github"
},
"original": {
diff --git a/scripts/update-charon-pin.sh b/scripts/update-charon-pin.sh
index 1fa706ae..304b2d83 100755
--- a/scripts/update-charon-pin.sh
+++ b/scripts/update-charon-pin.sh
@@ -5,7 +5,7 @@ if ! which jq 2> /dev/null 1>&2; then
fi
if [ -L charon ]; then
- echo '`./charon` is a symlink; we using the commit there for our new pin.'
+ echo '`./charon` is a symlink; we will use the commit there for our new pin.'
COMMIT="$(git -C charon rev-parse HEAD)"
nix flake lock --override-input charon "github:aeneasverif/charon/$COMMIT"
else
diff --git a/tests/src/mutually-recursive-traits.lean.out b/tests/src/mutually-recursive-traits.lean.out
index dffbb470..df80ccc6 100644
--- a/tests/src/mutually-recursive-traits.lean.out
+++ b/tests/src/mutually-recursive-traits.lean.out
@@ -11,7 +11,7 @@ Uncaught exception:
Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 47, characters 4-76
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
-Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 836, characters 2-52
-Called from Aeneas__Translate.extract_file in file "Translate.ml", line 963, characters 2-36
-Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1512, characters 5-42
+Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 839, characters 2-52
+Called from Aeneas__Translate.extract_file in file "Translate.ml", line 966, characters 2-36
+Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1515, characters 5-42
Called from Dune__exe__Main in file "Main.ml", line 317, characters 14-66
--
cgit v1.2.3