diff options
author | Escherichia | 2024-06-04 15:27:33 +0200 |
---|---|---|
committer | GitHub | 2024-06-04 15:27:33 +0200 |
commit | 5b7fc57cdc6bc5cff8373e6aa8df383278c9cf63 (patch) | |
tree | f5444d20797c05740ff8475c63ebc913df9dd393 | |
parent | afc4e62ce7a584da0bb0a7350533e321388be545 (diff) |
Propagated changes to statement from Charon (#223)
Co-authored-by: Escherichia <escherichia@charlotte>
Co-authored-by: Nadrieril <nadrieril+git@gmail.com>
Diffstat (limited to '')
-rw-r--r-- | charon-pin | 2 | ||||
-rw-r--r-- | compiler/InterpreterStatements.ml | 1 | ||||
-rw-r--r-- | compiler/PrePasses.ml | 2 | ||||
-rw-r--r-- | flake.lock | 6 |
4 files changed, 6 insertions, 5 deletions
@@ -1,2 +1,2 @@ # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas. -ae610b59b337b191d23f4f1c738ed290b8edd0d2 +438acf2ad2c6f7e03a16f8b1dc1bc3df96e72ae8 diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 5ddc1ed8..283a711d 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -1021,6 +1021,7 @@ and eval_statement_raw (config : config) (st : statement) : stl_cm_fun = let eval_loop_body = eval_statement config loop_body in InterpreterLoops.eval_loop config st.span eval_loop_body ctx | Switch switch -> eval_switch config st.span switch ctx + | Error s -> craise __FILE__ __LINE__ st.span s and eval_global (config : config) (span : Meta.span) (dest : place) (gid : GlobalDeclId.id) (generics : generic_args) : stl_cm_fun = diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml index 26141c72..9eb3b712 100644 --- a/compiler/PrePasses.ml +++ b/compiler/PrePasses.ml @@ -100,7 +100,7 @@ let remove_useless_cf_merges (crate : crate) (f : fun_decl) : fun_decl = let rec can_be_moved_aux (must_end_with_exit : bool) (st : statement) : bool = match st.content with | SetDiscriminant _ | Assert _ | Call _ | Break _ | Continue _ | Switch _ - | Loop _ -> + | Loop _ | Error _ -> false | Assign (_, rv) -> ( match rv with @@ -9,11 +9,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1717443886, - "narHash": "sha256-6tX6AgXQlIIuiKLOij0H2mf00rhU02hbQhs3lTARgMk=", + "lastModified": 1717506811, + "narHash": "sha256-QYPXD3+INGmfY9VA+X7ruRAeiU/siJYSHYAwXUOUNGM=", "owner": "aeneasverif", "repo": "charon", - "rev": "ae610b59b337b191d23f4f1c738ed290b8edd0d2", + "rev": "438acf2ad2c6f7e03a16f8b1dc1bc3df96e72ae8", "type": "github" }, "original": { |