diff options
Diffstat (limited to 'compiler')
-rw-r--r-- | compiler/Errors.ml | 16 | ||||
-rw-r--r-- | compiler/Extract.ml | 5 | ||||
-rw-r--r-- | compiler/Logging.ml | 3 |
3 files changed, 18 insertions, 6 deletions
diff --git a/compiler/Errors.ml b/compiler/Errors.ml index 04fd708b..53e56c44 100644 --- a/compiler/Errors.ml +++ b/compiler/Errors.ml @@ -1,3 +1,5 @@ +let log = Logging.errors_log + let meta_to_string (span : Meta.span) = let file = match span.file with Virtual s | Local s -> s in let loc_to_string (l : Meta.loc) : string = @@ -14,7 +16,7 @@ let format_error_message (meta : Meta.meta option) (msg : string) = let format_error_message_with_file_line (file : string) (line : int) (meta : Meta.meta option) (msg : string) = - "In file:" ^ file ^ ", line:" ^ string_of_int line ^ "\n" + "In file " ^ file ^ ", line " ^ string_of_int line ^ ":\n" ^ format_error_message meta msg exception CFailure of (Meta.meta option * string) @@ -28,13 +30,17 @@ let push_error (meta : Meta.meta option) (msg : string) = let save_error (file : string) (line : int) ?(throw : bool = false) (meta : Meta.meta option) (msg : string) = push_error meta msg; - if !Config.fail_hard && throw then - raise (Failure (format_error_message_with_file_line file line meta msg)) + if !Config.fail_hard && throw then ( + let msg = format_error_message_with_file_line file line meta msg in + log#serror (msg ^ "\n"); + raise (Failure msg)) let craise_opt_meta (file : string) (line : int) (meta : Meta.meta option) (msg : string) = - if !Config.fail_hard then - raise (Failure (format_error_message_with_file_line file line meta msg)) + if !Config.fail_hard then ( + let msg = format_error_message_with_file_line file line meta msg in + log#serror (msg ^ "\n"); + raise (Failure (format_error_message_with_file_line file line meta msg))) else let () = push_error meta msg in raise (CFailure (meta, msg)) diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 1a9b3baa..ad204f7a 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -2234,7 +2234,10 @@ let extract_trait_impl_register_names (ctx : extraction_ctx) (* For now we do not support overriding provided methods *) cassert __FILE__ __LINE__ (trait_impl.provided_methods = []) - trait_impl.meta "Overriding provided methods is not supported yet"; + trait_impl.meta + ("Overriding provided methods is not supported yet (overriden methods: " + ^ String.concat ", " (List.map fst trait_impl.provided_methods) + ^ ")"); (* Everything is taken care of by {!extract_trait_decl_register_names} *but* the name of the implementation itself *) (* Compute the name *) diff --git a/compiler/Logging.ml b/compiler/Logging.ml index 9c20f32f..9b8019b2 100644 --- a/compiler/Logging.ml +++ b/compiler/Logging.ml @@ -3,6 +3,9 @@ include Charon.Logging (** Below, we create subgloggers for various submodules, so that we can precisely toggle logging on/off, depending on which information we need *) +(** Logger for Errors *) +let errors_log = L.get_logger "MainLogger.Errors" + (** Logger for PrePasses *) let pre_passes_log = L.get_logger "MainLogger.PrePasses" |