diff options
| -rw-r--r-- | charon-pin | 2 | ||||
| -rw-r--r-- | compiler/FunsAnalysis.ml | 7 | ||||
| -rw-r--r-- | compiler/Interpreter.ml | 2 | ||||
| -rw-r--r-- | compiler/Print.ml | 1 | ||||
| -rw-r--r-- | compiler/Translate.ml | 3 | ||||
| -rw-r--r-- | flake.lock | 6 | ||||
| -rwxr-xr-x | scripts/update-charon-pin.sh | 2 | ||||
| -rw-r--r-- | tests/src/mutually-recursive-traits.lean.out | 6 |
8 files changed, 19 insertions, 10 deletions
@@ -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 @@ -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 |