diff options
| author | Escherichia | 2024-03-27 10:22:06 +0100 |
|---|---|---|
| committer | Escherichia | 2024-03-28 15:35:20 +0100 |
| commit | 0f0082c81db8852dff23cd4691af19c434c8be78 (patch) | |
| tree | eaf4c6e6faaceaeaf86e47b7b61249f86c08f65d /compiler/ExtractBase.ml | |
| parent | c47e349dedaaf0e3161869740ea769332ffd24ca (diff) | |
Added sanity_check and sanity_check_opt_meta helpers and changed sanity checks related cassert to these helpers to have a proper error message
Diffstat (limited to 'compiler/ExtractBase.ml')
| -rw-r--r-- | compiler/ExtractBase.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index c2e3e35f..1c21e99c 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -1904,7 +1904,7 @@ let ctx_compute_fun_name (def : fun_decl) (ctx : extraction_ctx) : string = let ctx_add_fun_decl (def : fun_decl) (ctx : extraction_ctx) : extraction_ctx = (* Sanity check: the function should not be a global body - those are handled * separately *) - cassert (not def.is_global_decl_body) def.meta "The function should not be a global body - those are handled separately"; + sanity_check (not def.is_global_decl_body) def.meta; (* Lookup the LLBC def to compute the region group information *) let def_id = def.def_id in (* Add the function name *) |