diff --git a/infer/src/clang/cFrontend.ml b/infer/src/clang/cFrontend.ml index 84927dddb..4562de8a8 100644 --- a/infer/src/clang/cFrontend.ml +++ b/infer/src/clang/cFrontend.ml @@ -31,7 +31,7 @@ let compute_icfg trans_unit_ctx tenv ast = assert false -(* NOTE: Assumes that an AST alsways starts with a TranslationUnitDecl *) +(* NOTE: Assumes that an AST always starts with a TranslationUnitDecl *) let init_global_state_capture () = Ident.NameGenerator.reset () ; @@ -66,5 +66,9 @@ let do_source_file translation_unit_context ast = Dotty.print_icfg_dotty source_file cfg ; Cg.save_call_graph_dotty source_file call_graph ) ; L.(debug Capture Verbose) "%a" Cfg.pp_proc_signatures cfg ; + L.(debug Capture Verbose) + "# Procedures started: %d@\n# Procedures completed: %d@\n@\n" + !CFrontend_config.procedures_attempted + (!CFrontend_config.procedures_attempted - !CFrontend_config.procedures_failed) ; (* NOTE: nothing should be written to source_dir after this *) DB.mark_file_updated (DB.source_dir_to_string source_dir) diff --git a/infer/src/clang/cFrontend_config.ml b/infer/src/clang/cFrontend_config.ml index f7f08d94b..a7d813328 100644 --- a/infer/src/clang/cFrontend_config.ml +++ b/infer/src/clang/cFrontend_config.ml @@ -173,11 +173,17 @@ let log_out = ref Format.std_formatter let sil_types_map = ref Clang_ast_extend.TypePointerMap.empty +let procedures_attempted = ref 0 + +let procedures_failed = ref 0 + let reset_global_state () = enum_map := ClangPointers.Map.empty ; global_translation_unit_decls := [] ; log_out := Format.std_formatter ; - sil_types_map := Clang_ast_extend.TypePointerMap.empty + sil_types_map := Clang_ast_extend.TypePointerMap.empty ; + procedures_attempted := 0 ; + procedures_failed := 0 let tableaux_evaluation = false diff --git a/infer/src/clang/cFrontend_config.mli b/infer/src/clang/cFrontend_config.mli index 423faede6..969875a75 100644 --- a/infer/src/clang/cFrontend_config.mli +++ b/infer/src/clang/cFrontend_config.mli @@ -173,6 +173,10 @@ val sil_types_map : Typ.desc Clang_ast_extend.TypePointerMap.t ref (** Map from type pointers (clang pointers and types created later by frontend) to sil types Populated during frontend execution when new type is found *) +val procedures_attempted : int ref + +val procedures_failed : int ref + val reset_global_state : unit -> unit val tableaux_evaluation : bool diff --git a/infer/src/clang/cFrontend_decl.ml b/infer/src/clang/cFrontend_decl.ml index 5b5b178f3..5c34a1d1d 100644 --- a/infer/src/clang/cFrontend_decl.ml +++ b/infer/src/clang/cFrontend_decl.ml @@ -17,6 +17,7 @@ module L = Logging let protect ~f ~recover ~pp_context = let log_and_recover ~print fmt = recover () ; + incr CFrontend_config.procedures_failed ; (if print then L.internal_error else L.(debug Capture Quiet)) ("%a@\n" ^^ fmt) pp_context () in try f () with @@ -48,6 +49,7 @@ module CFrontend_decl_funct (T : CModule_type.CTranslation) : CModule_type.CFron body has_return_param is_objc_method outer_context_opt extra_instrs = L.(debug Capture Verbose) "@\n@\n>>---------- ADDING METHOD: '%a' ---------<<@\n@\n" Typ.Procname.pp procname ; + incr CFrontend_config.procedures_attempted ; let recover () = Cfg.remove_proc_desc cfg procname ; CMethod_trans.create_external_procdesc cfg procname is_objc_method None