diff options
| author | Son HO | 2024-04-04 16:09:48 +0200 |
|---|---|---|
| committer | GitHub | 2024-04-04 16:09:48 +0200 |
| commit | 061d7f72bec27de46245afc82149271ca8c75627 (patch) | |
| tree | addd12dec0c1f5a564f9204fda77301771ff5e46 /compiler/SymbolicToPure.ml | |
| parent | 3909a38f3f8c58c9f97d36777c52e02617ef70b4 (diff) | |
| parent | 77208249c717579d1014f27592566069b8cd0eb2 (diff) | |
Merge pull request #106 from AeneasVerif/escherichia/error_catching
Added Error and EError to expressions and propagated related changes
Diffstat (limited to '')
| -rw-r--r-- | compiler/SymbolicToPure.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 5cd13072..f036cc37 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -1981,6 +1981,9 @@ let eval_ctx_to_symbolic_assignments_info (ctx : bs_ctx) (* Return the computed information *) !info +let translate_error (meta : Meta.meta option) (msg : string) : texpression = + { e = EError (meta, msg); ty = Error } + let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression = match e with | S.Return (ectx, opt_v) -> @@ -2007,6 +2010,7 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression = *) translate_forward_end ectx loop_input_values e back_e ctx | Loop loop -> translate_loop loop ctx + | Error (meta, msg) -> translate_error meta msg and translate_panic (ctx : bs_ctx) : texpression = (* Here we use the function return type - note that it is ok because |