Skip to content

Update charon #565

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
Jul 4, 2025
Merged

Update charon #565

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.
ccaf6c6f718487192ecad3ce447c161835a61262
91b5a914e7f6fb78fd26ff6bafed05676e5f8d33
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.

8 changes: 5 additions & 3 deletions src/PrePasses.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -652,8 +652,10 @@ let remove_shallow_borrows_storage_live_dead (crate : crate) (f : fun_decl) :
f

(** `StorageDead`, `Deinit` and `Drop` have the same semantics as far as Aeneas
is concerned: they store bottom in the place. This maps all three to `Drop`
is concerned: they store bottom in the place. This maps all three to `Deinit`
to simplify later work.
Note: `Drop` actually also calls code to deallocate the value; we decide to
ignore this for now.
*)
let unify_drops (f : fun_decl) : fun_decl =
let lookup_local (locals : locals) (var_id : local_id) : local =
Expand All @@ -663,12 +665,12 @@ let unify_drops (f : fun_decl) : fun_decl =
let unify_visitor =
object
inherit [_] map_statement
method! visit_Deinit _ p = Drop p
method! visit_Drop _ p _ = Deinit p

method! visit_StorageDead locals var_id =
let ty = (lookup_local locals var_id).var_ty in
let p = { kind = PlaceLocal var_id; ty } in
Drop p
Deinit p
end
in

Expand Down
6 changes: 3 additions & 3 deletions src/interp/InterpreterStatements.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -914,7 +914,7 @@ and eval_statement_raw (config : config) (st : statement) : stl_cm_fun =
| SetDiscriminant (p, variant_id) ->
let (ctx, res), cc = set_discriminant config st.span p variant_id ctx in
([ (ctx, res) ], cc_singleton __FILE__ __LINE__ st.span cc)
| Drop p ->
| Deinit p ->
let ctx, cc = drop_value config st.span p ctx in
([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ st.span cc)
| Assert assertion ->
Expand All @@ -933,9 +933,9 @@ and eval_statement_raw (config : config) (st : statement) : stl_cm_fun =
let eval_loop_body = eval_block config loop_body in
InterpreterLoops.eval_loop config st.span eval_loop_body ctx
| Switch switch -> eval_switch config st.span switch ctx
| Deinit _ | StorageDead _ ->
| Drop _ | StorageDead _ ->
craise __FILE__ __LINE__ st.span
"StorageDead/Deinit should have been removed in a prepass"
"StorageDead/Drop should have been removed in a prepass"
| Error s -> craise __FILE__ __LINE__ st.span s

and eval_global (config : config) (span : Meta.span) (dest : place)
Expand Down