diff --git a/infer/src/clang/ClangLogging.ml b/infer/src/clang/ClangLogging.ml
new file mode 100644
index 000000000..98d02bb75
--- /dev/null
+++ b/infer/src/clang/ClangLogging.ml
@@ -0,0 +1,24 @@
+(*
+ * Copyright (c) 2018 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+open! IStd
+module F = Format
+
+let log_caught_exception (trans_unit_ctx: CFrontend_config.translation_unit_context) exception_type
+    (exception_file, exception_line, _, _) (source_location_start, source_location_end) ast_node =
+  let caught_exception =
+    EventLogger.FrontendException
+      { exception_type
+      ; source_location_start= CLocation.clang_to_sil_location trans_unit_ctx source_location_start
+      ; source_location_end= CLocation.clang_to_sil_location trans_unit_ctx source_location_end
+      ; exception_file
+      ; exception_line
+      ; ast_node
+      ; lang= CFrontend_config.string_of_clang_lang trans_unit_ctx.lang }
+  in
+  EventLogger.log caught_exception
diff --git a/infer/src/clang/ClangLogging.mli b/infer/src/clang/ClangLogging.mli
new file mode 100644
index 000000000..67505a2ff
--- /dev/null
+++ b/infer/src/clang/ClangLogging.mli
@@ -0,0 +1,14 @@
+(*
+ * Copyright (c) 2018 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+
+open! IStd
+
+val log_caught_exception :
+  CFrontend_config.translation_unit_context -> string -> CFrontend_config.ocaml_pos
+  -> Clang_ast_t.source_location * Clang_ast_t.source_location -> string option -> unit
diff --git a/infer/src/clang/cAst_utils.ml b/infer/src/clang/cAst_utils.ml
index 15f128e6f..2166d94a2 100644
--- a/infer/src/clang/cAst_utils.ml
+++ b/infer/src/clang/cAst_utils.ml
@@ -135,13 +135,14 @@ let get_enum_constant_exp enum_constant_pointer =
   ClangPointers.Map.find_exn !CFrontend_config.enum_map enum_constant_pointer
 
 
-let get_type type_ptr =
-  (* There is chance for success only if type_ptr is in fact clang pointer *)
+let get_type ?source_range type_ptr =
+  let source_range = match source_range with Some sr -> sr | None -> dummy_source_range () in
   match type_ptr with
+  (* There is chance for success only if type_ptr is in fact clang pointer *)
   | Clang_ast_types.TypePtr.Ptr raw_ptr ->
       let typ = Int.Table.find ClangPointers.pointer_type_table raw_ptr in
       if Option.is_none typ then
-        CFrontend_config.incorrect_assumption __POS__ (dummy_source_range ())
+        CFrontend_config.incorrect_assumption __POS__ source_range
           "type with pointer %d not found@\n" raw_ptr ;
       typ
   | _ ->
@@ -151,8 +152,8 @@ let get_type type_ptr =
       None
 
 
-let get_desugared_type type_ptr =
-  let typ_opt = get_type type_ptr in
+let get_desugared_type ?source_range type_ptr =
+  let typ_opt = get_type ?source_range type_ptr in
   match typ_opt with
   | Some typ
     -> (
diff --git a/infer/src/clang/cAst_utils.mli b/infer/src/clang/cAst_utils.mli
index 63197b216..e8c692c01 100644
--- a/infer/src/clang/cAst_utils.mli
+++ b/infer/src/clang/cAst_utils.mli
@@ -52,10 +52,12 @@ val get_unqualified_name : Clang_ast_t.named_decl_info -> string
 val get_class_name_from_member : Clang_ast_t.named_decl_info -> QualifiedCppName.t
 (** returns qualified class name given member name info *)
 
-val get_type : Clang_ast_t.type_ptr -> Clang_ast_t.c_type option
+val get_type :
+  ?source_range:Clang_ast_t.source_range -> Clang_ast_t.type_ptr -> Clang_ast_t.c_type option
 (** looks up clang pointer to type and returns c_type. It requires type_ptr to be `TPtr. *)
 
-val get_desugared_type : Clang_ast_t.type_ptr -> Clang_ast_t.c_type option
+val get_desugared_type :
+  ?source_range:Clang_ast_t.source_range -> Clang_ast_t.type_ptr -> Clang_ast_t.c_type option
 (** looks up clang pointer to type and resolves any sugar around it.
     See get_type for more info and restrictions *)
 
diff --git a/infer/src/clang/cFrontend_config.ml b/infer/src/clang/cFrontend_config.ml
index ccb497213..95e303b8e 100644
--- a/infer/src/clang/cFrontend_config.ml
+++ b/infer/src/clang/cFrontend_config.ml
@@ -20,9 +20,11 @@ let string_of_clang_lang (lang: clang_lang) : string =
 
 let equal_clang_lang = [%compare.equal : clang_lang]
 
+type ocaml_pos = string * int * int * int
+
 type exception_details =
   { msg: string
-  ; position: string * int * int * int
+  ; position: ocaml_pos
   ; source_range: Clang_ast_t.source_range
   ; ast_node: string option }
 
@@ -37,7 +39,6 @@ exception IncorrectAssumption of exception_details
 let incorrect_assumption position source_range ?ast_node fmt =
   F.kasprintf (fun msg -> raise (IncorrectAssumption {msg; position; source_range; ast_node})) fmt
 
-
 type translation_unit_context = {lang: clang_lang; source_file: SourceFile.t}
 
 (** Constants *)
diff --git a/infer/src/clang/cFrontend_config.mli b/infer/src/clang/cFrontend_config.mli
index 079a45a64..84a9ed21c 100644
--- a/infer/src/clang/cFrontend_config.mli
+++ b/infer/src/clang/cFrontend_config.mli
@@ -17,16 +17,18 @@ val string_of_clang_lang : clang_lang -> string
 
 val equal_clang_lang : clang_lang -> clang_lang -> bool
 
+type ocaml_pos = string * int * int * int
+
 type exception_details =
   { msg: string
-  ; position: string * int * int * int
+  ; position: ocaml_pos
   ; source_range: Clang_ast_t.source_range
   ; ast_node: string option }
 
 exception Unimplemented of exception_details
 
 val unimplemented :
-  string * int * int * int -> Clang_ast_t.source_range -> ?ast_node:string
+  ocaml_pos -> Clang_ast_t.source_range -> ?ast_node:string
   -> ('a, Format.formatter, unit, _) format4 -> 'a
 (** Raise Unimplemented. This is caught at the level of translating a method and makes the frontend
     give up on that method. *)
@@ -34,7 +36,7 @@ val unimplemented :
 exception IncorrectAssumption of exception_details
 
 val incorrect_assumption :
-  string * int * int * int -> Clang_ast_t.source_range -> ?ast_node:string
+  ocaml_pos -> Clang_ast_t.source_range -> ?ast_node:string
   -> ('a, Format.formatter, unit, _) format4 -> 'a
 (** Used to mark places in the frontend that incorrectly assume something to be
     impossible. TODO(t21762295) get rid of all instances of this. *)
diff --git a/infer/src/clang/cFrontend_decl.ml b/infer/src/clang/cFrontend_decl.ml
index 065d0b0cd..9560eba62 100644
--- a/infer/src/clang/cFrontend_decl.ml
+++ b/infer/src/clang/cFrontend_decl.ml
@@ -20,41 +20,24 @@ let protect ~f ~recover ~pp_context (trans_unit_ctx: CFrontend_config.translatio
     incr CFrontend_config.procedures_failed ;
     (if print then L.internal_error else L.(debug Capture Quiet)) ("%a@\n" ^^ fmt) pp_context ()
   in
-  let caught_exception exception_type (exception_file, exception_line, _, _)
-      (source_location_start, source_location_end) ast_node =
-    EventLogger.FrontendException
-      { exception_type
-      ; source_location_start= CLocation.clang_to_sil_location trans_unit_ctx source_location_start
-      ; source_location_end= CLocation.clang_to_sil_location trans_unit_ctx source_location_end
-      ; exception_file
-      ; exception_line
-      ; ast_node
-      ; lang= CFrontend_config.string_of_clang_lang trans_unit_ctx.lang }
-  in
   try f () with
   (* Always keep going in case of known limitations of the frontend, crash otherwise (by not
        catching the exception) unless `--keep-going` was passed. Print errors we should fix
        (t21762295) to the console. *)
   | CFrontend_config.Unimplemented e ->
-      let caught_unimplemented_exception =
-        caught_exception "Unimplemented" e.position e.source_range e.ast_node
-      in
-      EventLogger.log caught_unimplemented_exception ;
+      ClangLogging.log_caught_exception trans_unit_ctx "Unimplemented" e.position e.source_range
+        e.ast_node ;
       log_and_recover ~print:false "Unimplemented feature:@\n  %s@\n" e.msg
   | CFrontend_config.IncorrectAssumption e ->
       (* FIXME(t21762295): we do not expect this to happen but it does *)
-      let caught_incorrect_assumption =
-        caught_exception "IncorrectAssumption" e.position e.source_range e.ast_node
-      in
-      EventLogger.log caught_incorrect_assumption ;
+      ClangLogging.log_caught_exception trans_unit_ctx "IncorrectAssumption" e.position
+        e.source_range e.ast_node ;
       log_and_recover ~print:true "Known incorrect assumption in the frontend: %s@\n" e.msg
   | CTrans_utils.Self.SelfClassException e ->
       (* FIXME(t21762295): we do not expect this to happen but it does *)
-      let caught_selfclass_exception =
-        Some (Typ.Name.to_string e.class_name)
-        |> caught_exception "SelfClassException" e.position e.source_range
-      in
-      EventLogger.log caught_selfclass_exception ;
+      Some (Typ.Name.to_string e.class_name)
+      |> ClangLogging.log_caught_exception trans_unit_ctx "SelfClassException" e.position
+           e.source_range ;
       log_and_recover ~print:true "Unexpected SelfClassException %a@\n" Typ.Name.pp e.class_name
   | exn ->
       let trace = Backtrace.get () in
diff --git a/infer/src/clang/cPredicates.ml b/infer/src/clang/cPredicates.ml
index d43bdb0ac..d80ad650d 100644
--- a/infer/src/clang/cPredicates.ml
+++ b/infer/src/clang/cPredicates.ml
@@ -708,7 +708,11 @@ let has_type_const_ptr_to_objc_class node =
   let open Clang_ast_t in
   match get_ast_node_type_ptr node with
   | Some type_ptr -> (
-    match CAst_utils.get_desugared_type type_ptr with
+    match
+      CAst_utils.get_desugared_type
+        ~source_range:(Ctl_parser_types.ast_node_source_range node)
+        type_ptr
+    with
     | Some ObjCObjectPointerType (_, qt) ->
         qt.qt_is_const
     | _ ->
diff --git a/infer/src/clang/cTL.ml b/infer/src/clang/cTL.ml
index 552f07275..8c860a403 100644
--- a/infer/src/clang/cTL.ml
+++ b/infer/src/clang/cTL.ml
@@ -1209,8 +1209,13 @@ and eval_formula f an lcxt : Ctl_parser_types.ast_node option =
         Some an
     | False ->
         None
-    | Atomic (name, params) ->
-        if eval_Atomic name params an lcxt then Some an else None
+    | Atomic (name, params) -> (
+      try if eval_Atomic name params an lcxt then Some an else None
+      with CFrontend_config.IncorrectAssumption e ->
+        let trans_unit_ctx = lcxt.CLintersContext.translation_unit_context in
+        ClangLogging.log_caught_exception trans_unit_ctx "IncorrectAssumption" e.position
+          e.source_range e.ast_node ;
+        None )
     | InNode (node_type_list, f1) ->
         in_node node_type_list f1 an lcxt
     | Not f1 -> (
diff --git a/infer/src/clang/ctl_parser_types.ml b/infer/src/clang/ctl_parser_types.ml
index 891cfaa74..4381d4897 100644
--- a/infer/src/clang/ctl_parser_types.ml
+++ b/infer/src/clang/ctl_parser_types.ml
@@ -90,6 +90,16 @@ let ast_node_kind node =
       Clang_ast_proj.get_decl_kind_string decl
 
 
+let ast_node_source_range node =
+  match node with
+  | Stmt stmt ->
+      let s_stmt_info, _ = Clang_ast_proj.get_stmt_tuple stmt in
+      s_stmt_info.si_source_range
+  | Decl decl ->
+      let d_decl_info = Clang_ast_proj.get_decl_tuple decl in
+      d_decl_info.di_source_range
+
+
 (* true iff an ast node is a node of type among the list tl *)
 let ast_node_has_kind tl an =
   let an_alexp = ALVar.Const (ast_node_kind an) in
diff --git a/infer/src/clang/ctl_parser_types.mli b/infer/src/clang/ctl_parser_types.mli
index 2248b435a..f50d0ac37 100644
--- a/infer/src/clang/ctl_parser_types.mli
+++ b/infer/src/clang/ctl_parser_types.mli
@@ -31,6 +31,8 @@ val stmt_node_child_type : ast_node -> string
 
 val ast_node_cast_kind : ast_node -> string
 
+val ast_node_source_range : ast_node -> Clang_ast_t.source_range
+
 val is_node_successor_of : is_successor:ast_node -> ast_node -> bool
 
 val get_direct_successor_nodes : ast_node -> ast_node list