diff options
author | Son HO | 2024-04-07 15:09:58 +0200 |
---|---|---|
committer | GitHub | 2024-04-07 15:09:58 +0200 |
commit | 05164f1ea87b7da14f60e6dbcc718a4f8d639ea1 (patch) | |
tree | 7973a53f134c38a856376b6204a7c76900eaafe7 /compiler/Invariants.ml | |
parent | d8650bfc5c4dc78fda13953dac93c9e6c24489d1 (diff) | |
parent | a9a2f81e365eeef4fd157fb56cd5107f95c91163 (diff) |
Merge pull request #113 from AeneasVerif/escherichia/error_catching_translate
Error catching should tell when code couldn't be generated
Diffstat (limited to '')
-rw-r--r-- | compiler/Invariants.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml index 642d7a37..2ccf3ad4 100644 --- a/compiler/Invariants.ml +++ b/compiler/Invariants.ml @@ -185,7 +185,6 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : "find_info: could not find the representant of borrow " ^ BorrowId.to_string bid ^ ":\nContext:\n" ^ context_to_string () in - log#serror err; craise __FILE__ __LINE__ meta err in @@ -706,13 +705,13 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = | AEndedProjBorrows _ | AIgnoredProjBorrows -> ()) | AIgnored, _ -> () | _ -> - log#lerror + log#ltrace (lazy ("Erroneous typing:" ^ "\n- raw value: " ^ show_typed_avalue atv ^ "\n- value: " ^ typed_avalue_to_string ~meta:(Some meta) ctx atv ^ "\n- type: " ^ ty_to_string ctx atv.ty)); - craise __FILE__ __LINE__ meta "Erroneous typing"); + internal_error __FILE__ __LINE__ meta); (* Continue exploring to inspect the subterms *) super#visit_typed_avalue info atv end |