Skip to content

Bump Charon #662

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Nadrieril merged 1 commit into from
Dec 2, 2025
Merged

Bump Charon #662

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion charon-pin
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
# This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
9f447cddf5ceaf5065f12e4a5c233ec497452005
377317d6b25702c46ffff072fa00a3e32095e46f
6 changes: 3 additions & 3 deletions flake.lock
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

18 changes: 9 additions & 9 deletions src/interp/InterpStatements.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -411,9 +411,9 @@ let eval_builtin_function_call_concrete (config : config) (span : Meta.span)
let args = call.args in
let dest = call.dest in
match call.func with
| FnOpMove _ ->
(* Closure case: TODO *)
[%craise] span "Closures are not supported yet"
| FnOpDynamic _ ->
(* Function pointer case: TODO *)
[%craise] span "Function pointers are not supported yet"
| FnOpRegular func ->
let generics = func.generics in
(* Sanity check: we don't fully handle the const generic vars environment
Expand Down Expand Up @@ -613,9 +613,9 @@ let eval_non_builtin_function_call_symbolic_inst (span : Meta.span)
(call : call) (ctx : eval_ctx) :
fn_ptr_kind * generic_args * fun_decl * inst_fun_sig =
match call.func with
| FnOpMove _ ->
(* Closure case: TODO *)
[%craise] span "Closures are not supported yet"
| FnOpDynamic _ ->
(* Function pointer case: TODO *)
[%craise] span "Function pointers are not supported yet"
| FnOpRegular func ->
let fid, generics, tr_self =
match func.kind with
Expand Down Expand Up @@ -1257,7 +1257,7 @@ and eval_function_call_concrete (config : config) (span : Meta.span)
(call : call) : stl_cm_fun =
fun ctx ->
match call.func with
| FnOpMove _ -> [%craise] span "Closures are not supported yet"
| FnOpDynamic _ -> [%craise] span "Function pointers are not supported yet"
| FnOpRegular func -> (
match func.kind with
| FunId (FRegular fid) ->
Expand All @@ -1276,7 +1276,7 @@ and eval_function_call_concrete (config : config) (span : Meta.span)
and eval_function_call_symbolic (config : config) (span : Meta.span)
(call : call) : stl_cm_fun =
match call.func with
| FnOpMove _ -> [%craise] span "Closures are not supported yet"
| FnOpDynamic _ -> [%craise] span "Function pointers are not supported yet"
| FnOpRegular func -> (
match func.kind with
| FunId (FRegular _) | TraitMethod _ ->
Expand All @@ -1292,7 +1292,7 @@ and eval_non_builtin_function_call_concrete (config : config) (span : Meta.span)
let args = call.args in
let dest = call.dest in
match call.func with
| FnOpMove _ -> [%craise] span "Closures are not supported yet"
| FnOpDynamic _ -> [%craise] span "Function pointers are not supported yet"
| FnOpRegular func ->
let generics = func.generics in
(* Sanity check: we don't fully handle the const generic vars environment
Expand Down
2 changes: 1 addition & 1 deletion src/llbc/FunsAnalysis.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -124,7 +124,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) :

method! visit_Call env call =
(match call.func with
| FnOpMove _ ->
| FnOpDynamic _ ->
(* Ignoring this: we lookup the called function upon creating
the closure *)
()
Expand Down