From 213fe46c893bacde2f7f9197792f3e87ef31695c Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Sun, 10 Apr 2016 13:43:37 -0700 Subject: [PATCH] Move ml_loc and operations to Logging Summary:public Refactor the ml_loc type and associated operations from Utils to Logging. Seems a better fit, and reduces dependencies. Reviewed By: cristianoc Differential Revision: D3161440 fb-gh-sync-id: 2e09c25 fbshipit-source-id: 2e09c25 --- infer/src/backend/errlog.ml | 4 +- infer/src/backend/errlog.mli | 2 +- infer/src/backend/exceptions.ml | 86 ++++++++++++++++---------------- infer/src/backend/exceptions.mli | 85 +++++++++++++++---------------- infer/src/backend/interproc.ml | 2 +- infer/src/backend/logging.ml | 22 ++++++++ infer/src/backend/logging.mli | 12 +++++ infer/src/backend/prop.ml | 2 +- infer/src/backend/prop.mli | 2 +- infer/src/backend/symExec.ml | 2 +- infer/src/backend/tabulation.mli | 2 +- infer/src/backend/utils.ml | 22 -------- infer/src/backend/utils.mli | 12 ----- 13 files changed, 128 insertions(+), 127 deletions(-) diff --git a/infer/src/backend/errlog.ml b/infer/src/backend/errlog.ml index 057513a5c..500d213bd 100644 --- a/infer/src/backend/errlog.ml +++ b/infer/src/backend/errlog.ml @@ -23,7 +23,7 @@ type loc_trace = loc_trace_elem list (** Data associated to a specific error *) type err_data = - (int * int) * int * Location.t * ml_loc option * loc_trace * + (int * int) * int * Location.t * L.ml_loc option * loc_trace * Prop.normal Prop.t option * Exceptions.err_class let err_data_compare @@ -65,7 +65,7 @@ let empty () = ErrLogHash.create 13 type iter_fun = (int * int) -> Location.t -> - ml_loc option -> + L.ml_loc option -> Exceptions.err_kind -> bool -> Localise.t -> Localise.error_desc -> string -> diff --git a/infer/src/backend/errlog.mli b/infer/src/backend/errlog.mli index d980baa7c..0329cbdc8 100644 --- a/infer/src/backend/errlog.mli +++ b/infer/src/backend/errlog.mli @@ -30,7 +30,7 @@ val empty : unit -> t type iter_fun = (int * int) -> Location.t -> - ml_loc option -> + Logging.ml_loc option -> Exceptions.err_kind -> bool -> Localise.t -> Localise.error_desc -> string -> diff --git a/infer/src/backend/exceptions.ml b/infer/src/backend/exceptions.ml index 011886a17..110eb846a 100644 --- a/infer/src/backend/exceptions.ml +++ b/infer/src/backend/exceptions.ml @@ -28,59 +28,59 @@ type err_class = Checker | Prover | Nocat type err_kind = Kwarning | Kerror | Kinfo -exception Abduction_case_not_implemented of ml_loc -exception Analysis_stops of Localise.error_desc * ml_loc option -exception Array_out_of_bounds_l1 of Localise.error_desc * ml_loc -exception Array_out_of_bounds_l2 of Localise.error_desc * ml_loc -exception Array_out_of_bounds_l3 of Localise.error_desc * ml_loc -exception Array_of_pointsto of ml_loc -exception Bad_footprint of ml_loc -exception Bad_pointer_comparison of Localise.error_desc * ml_loc -exception Class_cast_exception of Localise.error_desc * ml_loc +exception Abduction_case_not_implemented of L.ml_loc +exception Analysis_stops of Localise.error_desc * L.ml_loc option +exception Array_out_of_bounds_l1 of Localise.error_desc * L.ml_loc +exception Array_out_of_bounds_l2 of Localise.error_desc * L.ml_loc +exception Array_out_of_bounds_l3 of Localise.error_desc * L.ml_loc +exception Array_of_pointsto of L.ml_loc +exception Bad_footprint of L.ml_loc +exception Bad_pointer_comparison of Localise.error_desc * L.ml_loc +exception Class_cast_exception of Localise.error_desc * L.ml_loc exception Codequery of Localise.error_desc -exception Comparing_floats_for_equality of Localise.error_desc * ml_loc -exception Condition_is_assignment of Localise.error_desc * ml_loc -exception Condition_always_true_false of Localise.error_desc * bool * ml_loc -exception Context_leak of Localise.error_desc * ml_loc +exception Comparing_floats_for_equality of Localise.error_desc * L.ml_loc +exception Condition_is_assignment of Localise.error_desc * L.ml_loc +exception Condition_always_true_false of Localise.error_desc * bool * L.ml_loc +exception Context_leak of Localise.error_desc * L.ml_loc exception Custom_error of string * Localise.error_desc -exception Dangling_pointer_dereference of Sil.dangling_kind option * Localise.error_desc * ml_loc +exception Dangling_pointer_dereference of Sil.dangling_kind option * Localise.error_desc * L.ml_loc exception Deallocate_stack_variable of Localise.error_desc exception Deallocate_static_memory of Localise.error_desc -exception Deallocation_mismatch of Localise.error_desc * ml_loc -exception Divide_by_zero of Localise.error_desc * ml_loc +exception Deallocation_mismatch of Localise.error_desc * L.ml_loc +exception Divide_by_zero of Localise.error_desc * L.ml_loc exception Eradicate of string * Localise.error_desc -exception Field_not_null_checked of Localise.error_desc * ml_loc -exception Frontend_warning of string * Localise.error_desc * ml_loc +exception Field_not_null_checked of Localise.error_desc * L.ml_loc +exception Frontend_warning of string * Localise.error_desc * L.ml_loc exception Checkers of string * Localise.error_desc exception Inherently_dangerous_function of Localise.error_desc exception Internal_error of Localise.error_desc exception Java_runtime_exception of Typename.t * string * Localise.error_desc exception Leak of bool * Prop.normal Prop.t * Sil.hpred * (exception_visibility * Localise.error_desc) - * bool * Sil.resource * ml_loc -exception Missing_fld of Ident.fieldname * ml_loc -exception Premature_nil_termination of Localise.error_desc * ml_loc -exception Null_dereference of Localise.error_desc * ml_loc -exception Null_test_after_dereference of Localise.error_desc * ml_loc -exception Parameter_not_null_checked of Localise.error_desc * ml_loc -exception Pointer_size_mismatch of Localise.error_desc * ml_loc -exception Precondition_not_found of Localise.error_desc * ml_loc -exception Precondition_not_met of Localise.error_desc * ml_loc -exception Retain_cycle of Prop.normal Prop.t * Sil.hpred * Localise.error_desc * ml_loc -exception Registered_observer_being_deallocated of Localise.error_desc * ml_loc -exception Return_expression_required of Localise.error_desc * ml_loc -exception Return_statement_missing of Localise.error_desc * ml_loc -exception Return_value_ignored of Localise.error_desc * ml_loc + * bool * Sil.resource * L.ml_loc +exception Missing_fld of Ident.fieldname * L.ml_loc +exception Premature_nil_termination of Localise.error_desc * L.ml_loc +exception Null_dereference of Localise.error_desc * L.ml_loc +exception Null_test_after_dereference of Localise.error_desc * L.ml_loc +exception Parameter_not_null_checked of Localise.error_desc * L.ml_loc +exception Pointer_size_mismatch of Localise.error_desc * L.ml_loc +exception Precondition_not_found of Localise.error_desc * L.ml_loc +exception Precondition_not_met of Localise.error_desc * L.ml_loc +exception Retain_cycle of Prop.normal Prop.t * Sil.hpred * Localise.error_desc * L.ml_loc +exception Registered_observer_being_deallocated of Localise.error_desc * L.ml_loc +exception Return_expression_required of Localise.error_desc * L.ml_loc +exception Return_statement_missing of Localise.error_desc * L.ml_loc +exception Return_value_ignored of Localise.error_desc * L.ml_loc exception Skip_function of Localise.error_desc -exception Skip_pointer_dereference of Localise.error_desc * ml_loc -exception Stack_variable_address_escape of Localise.error_desc * ml_loc -exception Symexec_memory_error of ml_loc -exception Tainted_value_reaching_sensitive_function of Localise.error_desc * ml_loc -exception Unary_minus_applied_to_unsigned_expression of Localise.error_desc * ml_loc -exception Uninitialized_value of Localise.error_desc * ml_loc +exception Skip_pointer_dereference of Localise.error_desc * L.ml_loc +exception Stack_variable_address_escape of Localise.error_desc * L.ml_loc +exception Symexec_memory_error of L.ml_loc +exception Tainted_value_reaching_sensitive_function of Localise.error_desc * L.ml_loc +exception Unary_minus_applied_to_unsigned_expression of Localise.error_desc * L.ml_loc +exception Uninitialized_value of Localise.error_desc * L.ml_loc exception Unknown_proc -exception Use_after_free of Localise.error_desc * ml_loc -exception Wrong_argument_number of ml_loc +exception Use_after_free of Localise.error_desc * L.ml_loc +exception Wrong_argument_number of L.ml_loc (** Turn an exception into a descriptive string, error description, location in ml source, and category *) @@ -90,7 +90,7 @@ let recognize_exception exn = match Localise.error_desc_get_bucket desc with | None -> false | Some bucket -> bucket <> Localise.BucketLevel.b1 in - let err_name, desc, (ml_loc_opt : ml_loc option), visibility, severity, force_kind, eclass = + let err_name, desc, (ml_loc_opt : L.ml_loc option), visibility, severity, force_kind, eclass = match exn with (* all the names of Exn_user errors must be defined in Localise *) | Abduction_case_not_implemented ml_loc -> (Localise.from_string "Abduction_case_not_implemented", @@ -304,7 +304,7 @@ let print_exception_html s exn = let err_name, desc, ml_loc_opt, _, _, _, _ = recognize_exception exn in let ml_loc_string = match ml_loc_opt with | None -> "" - | Some ml_loc -> " " ^ ml_loc_to_string ml_loc in + | Some ml_loc -> " " ^ L.ml_loc_to_string ml_loc in let desc_str = pp_to_string Localise.pp_error_desc desc in (L.d_strln_color Red) (s ^ (Localise.to_string err_name) ^ " " ^ desc_str ^ ml_loc_string) @@ -334,7 +334,7 @@ let pp_err (_, node_key) loc ekind ex_name desc ml_loc_opt fmt () = Localise.pp ex_name Localise.pp_error_desc desc pp_key node_key - pp_ml_loc_opt ml_loc_opt + L.pp_ml_loc_opt ml_loc_opt (** Return true if the exception is not serious and should be handled in timeout mode *) let handle_exception exn = diff --git a/infer/src/backend/exceptions.mli b/infer/src/backend/exceptions.mli index 448cdf25a..77bf7d97c 100644 --- a/infer/src/backend/exceptions.mli +++ b/infer/src/backend/exceptions.mli @@ -27,59 +27,60 @@ type err_kind = (** class of error *) type err_class = Checker | Prover | Nocat -exception Abduction_case_not_implemented of ml_loc -exception Analysis_stops of Localise.error_desc * ml_loc option -exception Array_of_pointsto of ml_loc -exception Array_out_of_bounds_l1 of Localise.error_desc * ml_loc -exception Array_out_of_bounds_l2 of Localise.error_desc * ml_loc -exception Array_out_of_bounds_l3 of Localise.error_desc * ml_loc -exception Bad_footprint of ml_loc -exception Bad_pointer_comparison of Localise.error_desc * ml_loc -exception Class_cast_exception of Localise.error_desc * ml_loc +exception Abduction_case_not_implemented of Logging.ml_loc +exception Analysis_stops of Localise.error_desc * Logging.ml_loc option +exception Array_of_pointsto of Logging.ml_loc +exception Array_out_of_bounds_l1 of Localise.error_desc * Logging.ml_loc +exception Array_out_of_bounds_l2 of Localise.error_desc * Logging.ml_loc +exception Array_out_of_bounds_l3 of Localise.error_desc * Logging.ml_loc +exception Bad_footprint of Logging.ml_loc +exception Bad_pointer_comparison of Localise.error_desc * Logging.ml_loc +exception Class_cast_exception of Localise.error_desc * Logging.ml_loc exception Codequery of Localise.error_desc -exception Comparing_floats_for_equality of Localise.error_desc * ml_loc -exception Condition_always_true_false of Localise.error_desc * bool * ml_loc -exception Condition_is_assignment of Localise.error_desc * ml_loc -exception Context_leak of Localise.error_desc * ml_loc +exception Comparing_floats_for_equality of Localise.error_desc * Logging.ml_loc +exception Condition_always_true_false of Localise.error_desc * bool * Logging.ml_loc +exception Condition_is_assignment of Localise.error_desc * Logging.ml_loc +exception Context_leak of Localise.error_desc * Logging.ml_loc exception Custom_error of string * Localise.error_desc -exception Dangling_pointer_dereference of Sil.dangling_kind option * Localise.error_desc * ml_loc +exception Dangling_pointer_dereference of + Sil.dangling_kind option * Localise.error_desc * Logging.ml_loc exception Deallocate_stack_variable of Localise.error_desc exception Deallocate_static_memory of Localise.error_desc -exception Deallocation_mismatch of Localise.error_desc * ml_loc -exception Divide_by_zero of Localise.error_desc * ml_loc -exception Field_not_null_checked of Localise.error_desc * ml_loc +exception Deallocation_mismatch of Localise.error_desc * Logging.ml_loc +exception Divide_by_zero of Localise.error_desc * Logging.ml_loc +exception Field_not_null_checked of Localise.error_desc * Logging.ml_loc exception Eradicate of string * Localise.error_desc exception Checkers of string * Localise.error_desc -exception Frontend_warning of string * Localise.error_desc * ml_loc +exception Frontend_warning of string * Localise.error_desc * Logging.ml_loc exception Inherently_dangerous_function of Localise.error_desc exception Internal_error of Localise.error_desc exception Java_runtime_exception of Typename.t * string * Localise.error_desc exception Leak of bool * Prop.normal Prop.t * Sil.hpred * (exception_visibility * Localise.error_desc) - * bool * Sil.resource * ml_loc -exception Missing_fld of Ident.fieldname * ml_loc -exception Premature_nil_termination of Localise.error_desc * ml_loc -exception Null_dereference of Localise.error_desc * ml_loc -exception Null_test_after_dereference of Localise.error_desc * ml_loc -exception Parameter_not_null_checked of Localise.error_desc * ml_loc -exception Pointer_size_mismatch of Localise.error_desc * ml_loc -exception Precondition_not_found of Localise.error_desc * ml_loc -exception Precondition_not_met of Localise.error_desc * ml_loc -exception Retain_cycle of Prop.normal Prop.t * Sil.hpred * Localise.error_desc * ml_loc -exception Registered_observer_being_deallocated of Localise.error_desc * ml_loc -exception Return_expression_required of Localise.error_desc * ml_loc -exception Return_statement_missing of Localise.error_desc * ml_loc -exception Return_value_ignored of Localise.error_desc * ml_loc + * bool * Sil.resource * Logging.ml_loc +exception Missing_fld of Ident.fieldname * Logging.ml_loc +exception Premature_nil_termination of Localise.error_desc * Logging.ml_loc +exception Null_dereference of Localise.error_desc * Logging.ml_loc +exception Null_test_after_dereference of Localise.error_desc * Logging.ml_loc +exception Parameter_not_null_checked of Localise.error_desc * Logging.ml_loc +exception Pointer_size_mismatch of Localise.error_desc * Logging.ml_loc +exception Precondition_not_found of Localise.error_desc * Logging.ml_loc +exception Precondition_not_met of Localise.error_desc * Logging.ml_loc +exception Retain_cycle of Prop.normal Prop.t * Sil.hpred * Localise.error_desc * Logging.ml_loc +exception Registered_observer_being_deallocated of Localise.error_desc * Logging.ml_loc +exception Return_expression_required of Localise.error_desc * Logging.ml_loc +exception Return_statement_missing of Localise.error_desc * Logging.ml_loc +exception Return_value_ignored of Localise.error_desc * Logging.ml_loc exception Skip_function of Localise.error_desc -exception Skip_pointer_dereference of Localise.error_desc * ml_loc -exception Stack_variable_address_escape of Localise.error_desc * ml_loc -exception Symexec_memory_error of ml_loc -exception Tainted_value_reaching_sensitive_function of Localise.error_desc * ml_loc -exception Unary_minus_applied_to_unsigned_expression of Localise.error_desc * ml_loc -exception Uninitialized_value of Localise.error_desc * ml_loc +exception Skip_pointer_dereference of Localise.error_desc * Logging.ml_loc +exception Stack_variable_address_escape of Localise.error_desc * Logging.ml_loc +exception Symexec_memory_error of Logging.ml_loc +exception Tainted_value_reaching_sensitive_function of Localise.error_desc * Logging.ml_loc +exception Unary_minus_applied_to_unsigned_expression of Localise.error_desc * Logging.ml_loc +exception Uninitialized_value of Localise.error_desc * Logging.ml_loc exception Unknown_proc -exception Use_after_free of Localise.error_desc * ml_loc -exception Wrong_argument_number of ml_loc +exception Use_after_free of Localise.error_desc * Logging.ml_loc +exception Wrong_argument_number of Logging.ml_loc (** string describing an error class *) val err_class_string : err_class -> string @@ -96,10 +97,10 @@ val print_exception_html : string -> exn -> unit (** pretty print an error given its (id,key), location, kind, name, description, and optional ml location *) val pp_err : int * int -> Location.t -> err_kind -> Localise.t -> Localise.error_desc -> - ml_loc option -> Format.formatter -> unit -> unit + Logging.ml_loc option -> Format.formatter -> unit -> unit (** Turn an exception into an error name, error description, location in ml source, and category *) val recognize_exception : exn -> - (Localise.t * Localise.error_desc * (ml_loc option) * exception_visibility * + (Localise.t * Localise.error_desc * (Logging.ml_loc option) * exception_visibility * exception_severity * err_kind option * err_class) diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 12c5713b1..11443a8f4 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -1342,7 +1342,7 @@ let perform_transition exe_env tenv proc_name = L.err "Error in collect_preconditions for %a@." Procname.pp proc_name; let err_name, _, ml_loc_opt, _, _, _, _ = Exceptions.recognize_exception exn in let err_str = "exception raised " ^ (Localise.to_string err_name) in - L.err "Error: %s %a@." err_str pp_ml_loc_opt ml_loc_opt; + L.err "Error: %s %a@." err_str L.pp_ml_loc_opt ml_loc_opt; [] in transition_footprint_re_exe proc_name joined_pres in if Specs.get_phase proc_name == Specs.FOOTPRINT diff --git a/infer/src/backend/logging.ml b/infer/src/backend/logging.ml index 064c0ca13..354e6ccfc 100644 --- a/infer/src/backend/logging.ml +++ b/infer/src/backend/logging.ml @@ -129,6 +129,28 @@ let stderr fmt_string = let stdout fmt_string = do_print F.std_formatter fmt_string +(** Type of location in ml source: __POS__ *) +type ml_loc = string * int * int * int + +(** Convert a ml location to a string *) +let ml_loc_to_string (file, lnum, cnum, enum) = + Printf.sprintf "%s:%d:%d-%d:" file lnum cnum enum + +(** Pretty print a location of ml source *) +let pp_ml_loc fmt ml_loc = + F.fprintf fmt "%s" (ml_loc_to_string ml_loc) + +let pp_ml_loc_opt fmt ml_loc_opt = + if !Config.developer_mode then match ml_loc_opt with + | None -> () + | Some ml_loc -> F.fprintf fmt "(%a)" pp_ml_loc ml_loc + +let assert_false ((file, lnum, cnum, _) as ml_loc) = + Printf.eprintf "\nASSERT FALSE %s\nCALL STACK\n%s\n%!" + (ml_loc_to_string ml_loc) + (Printexc.raw_backtrace_to_string (Printexc.get_callstack 1000)); + raise (Assert_failure (file, lnum, cnum)) + (** print a warning with information of the position in the ml source where it oririnated. use as: warning_position "description" (try assert false with Assert_failure x -> x); *) let warning_position (s: string) (ml_loc: ml_loc) = diff --git a/infer/src/backend/logging.mli b/infer/src/backend/logging.mli index edd26c474..75c1b7c6c 100644 --- a/infer/src/backend/logging.mli +++ b/infer/src/backend/logging.mli @@ -93,6 +93,18 @@ val set_err_formatter : Format.formatter -> unit (** Flush the current streams *) val flush_streams : unit -> unit +(** Type of location in ml source: __POS__ *) +type ml_loc = string * int * int * int + +(** Convert a ml location to a string *) +val ml_loc_to_string : ml_loc -> string + +(** Pretty print a location of ml source *) +val pp_ml_loc_opt : Format.formatter -> ml_loc option -> unit + +(** Print stack trace and throw assert false *) +val assert_false : ml_loc -> 'a + (** print a warning with information of the position in the ml source where it oririnated. use as: warning_position "description" (try assert false with Assert_failure x -> x); *) val warning_position: string -> ml_loc -> unit diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index f340206f8..4910b330c 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -46,7 +46,7 @@ type 'a t = foot_pi: pi; (** abduced pure part *) } -exception Cannot_star of ml_loc +exception Cannot_star of L.ml_loc (** {2 Basic Functions for Propositions} *) diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli index 7a9a87262..c2caed4e5 100644 --- a/infer/src/backend/prop.mli +++ b/infer/src/backend/prop.mli @@ -29,7 +29,7 @@ type struct_init_mode = | No_init | Fld_init -exception Cannot_star of ml_loc +exception Cannot_star of Logging.ml_loc (** {2 Basic Functions for propositions} *) diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 40b9f27d9..dead77de4 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -1216,7 +1216,7 @@ and instrs ?(mask_errors=false) tenv pdesc instrs ppl = with exn when exn_not_failure exn && mask_errors -> let err_name, _, ml_source, _ , _, _, _ = Exceptions.recognize_exception exn in let loc = (match ml_source with - | Some ml_loc -> "at " ^ (ml_loc_to_string ml_loc) + | Some ml_loc -> "at " ^ (L.ml_loc_to_string ml_loc) | None -> "") in L.d_warning ("Generated Instruction Failed with: " ^ diff --git a/infer/src/backend/tabulation.mli b/infer/src/backend/tabulation.mli index c7c488aa2..03e3f41b2 100644 --- a/infer/src/backend/tabulation.mli +++ b/infer/src/backend/tabulation.mli @@ -26,7 +26,7 @@ val find_dereference_without_null_check_in_sexp : Sil.strexp -> (int * Sil.path_ (** raise a cast exception *) val raise_cast_exception : - ml_loc -> Procname.t option -> Sil.exp -> Sil.exp -> Sil.exp -> 'a + Logging.ml_loc -> Procname.t option -> Sil.exp -> Sil.exp -> Sil.exp -> 'a (** check if a prop is an exception *) val prop_is_exn : Procname.t -> 'a Prop.t -> bool diff --git a/infer/src/backend/utils.ml b/infer/src/backend/utils.ml index 8f02b845f..7c966dd67 100644 --- a/infer/src/backend/utils.ml +++ b/infer/src/backend/utils.ml @@ -237,22 +237,6 @@ let pp_elapsed_time fmt () = let elapsed = Unix.gettimeofday () -. initial_timeofday in Format.fprintf fmt "%f" elapsed -(** Type of location in ml source: __POS__ *) -type ml_loc = string * int * int * int - -(** Convert a ml location to a string *) -let ml_loc_to_string (file, lnum, cnum, enum) = - Printf.sprintf "%s:%d:%d-%d:" file lnum cnum enum - -(** Pretty print a location of ml source *) -let pp_ml_loc fmt ml_loc = - F.fprintf fmt "%s" (ml_loc_to_string ml_loc) - -let pp_ml_loc_opt fmt ml_loc_opt = - if !Config.developer_mode then match ml_loc_opt with - | None -> () - | Some ml_loc -> F.fprintf fmt "(%a)" pp_ml_loc ml_loc - (** {2 SymOp and Failures: units of symbolic execution} *) type failure_kind = @@ -1000,9 +984,3 @@ let run_in_footprint_mode f x = let run_with_abs_val_equal_zero f x = set_reference_and_call_function Config.abs_val 0 f x - -let assert_false ((file, lnum, cnum, _) as ml_loc) = - Printf.eprintf "\nASSERT FALSE %s\nCALL STACK\n%s\n%!" - (ml_loc_to_string ml_loc) - (Printexc.raw_backtrace_to_string (Printexc.get_callstack 1000)); - raise (Assert_failure (file, lnum, cnum)) diff --git a/infer/src/backend/utils.mli b/infer/src/backend/utils.mli index 537d14130..726d32881 100644 --- a/infer/src/backend/utils.mli +++ b/infer/src/backend/utils.mli @@ -68,15 +68,6 @@ module StringMap : Map.S with type key = string (** {2 Printing} *) -(** Type of location in ml source: __POS__ *) -type ml_loc = string * int * int * int - -(** Convert a ml location to a string *) -val ml_loc_to_string : ml_loc -> string - -(** Pretty print a location of ml source *) -val pp_ml_loc_opt : Format.formatter -> ml_loc option -> unit - (** Colors supported in printing *) type color = Black | Blue | Green | Orange | Red @@ -380,6 +371,3 @@ val run_in_re_execution_mode : ('a -> 'b) -> 'a -> 'b (** [set_reference_and_call_function ref val f x] calls f x with ref set to val. Restore the initial value also in case of exception. *) val set_reference_and_call_function : 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c - -(** Pritn stack trace and throw assert false *) -val assert_false : ml_loc -> 'a