diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index f96d3bc8b..7dd83b0c3 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -1246,6 +1246,7 @@ let report_unsafe_accesses ~is_file_threadsafe aggregated_access_map = let may_alias tenv p1 p2 = let open Typ in let open AccessPath in + phys_equal p1 p2 || match List.last_exn (snd p1), List.last_exn (snd p2) with | FieldAccess _, ArrayAccess _ | ArrayAccess _, FieldAccess _ -> false (* fields in Java contain the class name /declaring/ them @@ -1275,6 +1276,8 @@ let quotient_access_map acc_map = (* assumption: the tenv for k is sufficient for k' too *) let (k_part, non_k_part) = AccessListMap.partition (fun k' _ -> may_alias tenv k k') m in + if AccessListMap.is_empty k_part + then failwith "Error: may_alias is not reflexive!"; let k_accesses = AccessListMap.fold (fun _ v acc' -> List.append v acc')