From 7f446a42a81a3506ca14993498f1320b0e36d0cb Mon Sep 17 00:00:00 2001
From: Dominik Harmim <harmim6@gmail.com>
Date: Sat, 20 Mar 2021 20:58:30 +0100
Subject: [PATCH] Atomicity analysis

- Local atomicity violations (not actual violations because the functions with
  these violations are always called under the lock higher in the call
  hierarchy) are reported only as warnings.

- The atomic sets file is moved from 'infer-out/atomic-sets' to 'atomic-sets'.

- Definition of a type 't' and including of the 'PrettyPrintable.PrintableType'
  module in modules are replaced with including the
  'PrettyPrintable.PrintableEquatableOrderedType' module.
---
 infer/src/atomicity/AtomicSets.ml             |   6 +-
 infer/src/atomicity/AtomicSetsDomain.ml       | 179 +++++-----
 infer/src/atomicity/AtomicSetsDomain.mli      |   8 +-
 infer/src/atomicity/AtomicityUtils.ml         |  12 +-
 infer/src/atomicity/AtomicityUtils.mli        |  13 +-
 infer/src/atomicity/AtomicityViolations.ml    |  32 +-
 infer/src/atomicity/AtomicityViolations.mli   |   4 +
 .../atomicity/AtomicityViolationsDomain.ml    | 328 ++++++++++++------
 .../atomicity/AtomicityViolationsDomain.mli   |  22 +-
 infer/src/backend/registerCheckers.ml         |   5 +-
 infer/src/base/IssueType.ml                   |  11 +-
 infer/src/base/IssueType.mli                  |   4 +-
 infer/src/base/ResultsDirEntryName.ml         |   6 +
 infer/src/base/ResultsDirEntryName.mli        |   2 +
 14 files changed, 386 insertions(+), 246 deletions(-)

diff --git a/infer/src/atomicity/AtomicSets.ml b/infer/src/atomicity/AtomicSets.ml
index 8146075ba2d..e44f84b3c98 100644
--- a/infer/src/atomicity/AtomicSets.ml
+++ b/infer/src/atomicity/AtomicSets.ml
@@ -119,10 +119,8 @@ let analyse_procedure (analysis_data : Domain.Summary.t InterproceduralAnalysis.
           Procname.pp pName
 
 
-let print_atomic_sets (analysis_data : AtomicSetsDomain.Summary.t InterproceduralAnalysis.file_t) :
-    IssueLog.t =
-  (* Create a directory for printing. *)
-  Utils.create_dir inferDir ;
+let print_atomic_sets (analysis_data : Domain.Summary.t InterproceduralAnalysis.file_t) : IssueLog.t
+    =
   (* Print to a file. *)
   let oc : Out_channel.t =
     Out_channel.create ~binary:false ~append:Config.atomic_sets_file_append ~fail_if_exists:false
diff --git a/infer/src/atomicity/AtomicSetsDomain.ml b/infer/src/atomicity/AtomicSetsDomain.ml
index c294e743011..cbdba1d3934 100644
--- a/infer/src/atomicity/AtomicSetsDomain.ml
+++ b/infer/src/atomicity/AtomicSetsDomain.ml
@@ -10,16 +10,16 @@ module Set = Caml.Set
 (* ************************************ Types *************************************************** *)
 
 (** A pair of sets of calls. Calls without a lock followed by calls with a lock. *)
-type callsPair = SSet.t * SSet.t [@@deriving compare, equal]
+type calls_pair = SSet.t * SSet.t [@@deriving compare, equal]
 
 (** A pair of sets of calls with a lock. *)
-type callsPairLock = callsPair * Lock.t [@@deriving compare, equal]
+type calls_pair_lock = calls_pair * Lock.t [@@deriving compare, equal]
 
 (* ************************************ Modules ************************************************* *)
 
 (** A set of pairs of sets of calls. *)
 module CallsPairSet = Set.Make (struct
-  type t = callsPair [@@deriving compare, equal]
+  type t = calls_pair [@@deriving compare, equal]
 end)
 
 (** A set of sets of strings. *)
@@ -27,23 +27,23 @@ module SSSet = Set.Make (SSet)
 
 (** A set of pairs of sets of calls with locks. *)
 module CallsPairLockSet = Set.Make (struct
-  type t = callsPairLock [@@deriving compare, equal]
+  type t = calls_pair_lock [@@deriving compare, equal]
 end)
 
 (* ************************************ Astate ************************************************** *)
 
 (** An element of an abstract state. *)
-type tElement =
+type t_element =
   { calls: SSet.t
   ; callsPairs: CallsPairLockSet.t
   ; finalCallsPairs: CallsPairSet.t
-  ; allOccurrences: SSet.t list
+  ; allCalls: SSet.t list
   ; guards: Guards.t }
 [@@deriving compare, equal]
 
 (** A set of types tElement is an abstract state. *)
 module TSet = Set.Make (struct
-  type t = tElement [@@deriving compare, equal]
+  type t = t_element [@@deriving compare, equal]
 end)
 
 type t = TSet.t [@@deriving compare, equal]
@@ -69,49 +69,51 @@ let initial : t =
     { calls= SSet.empty
     ; callsPairs= CallsPairLockSet.empty
     ; finalCallsPairs= CallsPairSet.empty
-    ; allOccurrences= [SSet.empty]
+    ; allCalls= [SSet.empty]
     ; guards= Guards.empty }
 
 
 let pp (fmt : F.formatter) (astate : t) : unit =
   F.pp_print_string fmt "\n" ;
-  let iterator (astateEl : tElement) : unit =
+  let iterator (astateEl : t_element) : unit =
     F.pp_print_string fmt "{\n" ;
     (* calls *)
     F.fprintf fmt "\t{%s};\n" (String.concat (SSet.elements astateEl.calls) ~sep:", ") ;
     (* callsPairs *)
     F.pp_print_string fmt "\t" ;
-    let lastCallsPair : callsPairLock option = CallsPairLockSet.max_elt_opt astateEl.callsPairs in
-    let print_calls_pair (((pFst, pSnd), lock) as callsPair : callsPairLock) : unit =
+    let lastCallsPair : calls_pair_lock option = CallsPairLockSet.max_elt_opt astateEl.callsPairs in
+    let print_calls_pair (((pFst, pSnd), lock) as callsPair : calls_pair_lock) : unit =
       let withoutLock : string = String.concat (SSet.elements pFst) ~sep:", "
       and withLock : string = String.concat (SSet.elements pSnd) ~sep:", " in
-      F.fprintf fmt "%a{%s} ( {%s} )" Lock.pp lock withoutLock withLock ;
-      if not (equal_callsPairLock callsPair (Option.value_exn lastCallsPair)) then
+      F.fprintf fmt "%a: {%s} ( {%s} )" Lock.pp lock withoutLock withLock ;
+      if not (equal_calls_pair_lock callsPair (Option.value_exn lastCallsPair)) then
         F.pp_print_string fmt " | "
     in
     CallsPairLockSet.iter print_calls_pair astateEl.callsPairs ;
     F.pp_print_string fmt ";\n" ;
     (* finalCallsPairs *)
     F.pp_print_string fmt "\t" ;
-    let lastFinalCallsPair : callsPair option = CallsPairSet.max_elt_opt astateEl.finalCallsPairs in
-    let print_final_calls_pair ((pFst, pSnd) as callsPair : callsPair) : unit =
+    let lastFinalCallsPair : calls_pair option =
+      CallsPairSet.max_elt_opt astateEl.finalCallsPairs
+    in
+    let print_final_calls_pair ((pFst, pSnd) as callsPair : calls_pair) : unit =
       let withoutLock : string = String.concat (SSet.elements pFst) ~sep:", "
       and withLock : string = String.concat (SSet.elements pSnd) ~sep:", " in
       F.fprintf fmt "{%s} ( {%s} )" withoutLock withLock ;
-      if not (equal_callsPair callsPair (Option.value_exn lastFinalCallsPair)) then
+      if not (equal_calls_pair callsPair (Option.value_exn lastFinalCallsPair)) then
         F.pp_print_string fmt " | "
     in
     CallsPairSet.iter print_final_calls_pair astateEl.finalCallsPairs ;
     F.pp_print_string fmt ";\n" ;
-    (* allOccurrences *)
+    (* allCalls *)
     F.pp_print_string fmt "\t{\n" ;
-    let print_all_occurrences (i : int) (allOccurrences : SSet.t) : unit =
-      F.fprintf fmt "\t\t%i: {%s};\n" i (String.concat (SSet.elements allOccurrences) ~sep:", ")
+    let print_all_calls (i : int) (allCalls : SSet.t) : unit =
+      F.fprintf fmt "\t\t%i: {%s};\n" i (String.concat (SSet.elements allCalls) ~sep:", ")
     in
-    List.iteri astateEl.allOccurrences ~f:print_all_occurrences ;
+    List.iteri astateEl.allCalls ~f:print_all_calls ;
     F.pp_print_string fmt "\t};\n" ;
     (* guards *)
-    F.fprintf fmt "%a" Guards.pp astateEl.guards ;
+    F.fprintf fmt "\t{\n%a\t};\n" Guards.pp astateEl.guards ;
     F.pp_print_string fmt "}\n"
   in
   TSet.iter iterator astate ;
@@ -119,10 +121,10 @@ let pp (fmt : F.formatter) (astate : t) : unit =
 
 
 (** Modifies an element of an abstract state after addition of function calls. *)
-let update_astate_el_after_calls (astateEl : tElement) : tElement =
+let update_astate_el_after_calls (astateEl : t_element) : t_element =
   let finalCallsPairs : CallsPairSet.t ref = ref astateEl.finalCallsPairs in
   let callsPairs : CallsPairLockSet.t =
-    let filter (((pFst, pSnd), _) : callsPairLock) : bool =
+    let filter (((pFst, pSnd), _) : calls_pair_lock) : bool =
       if SSet.cardinal pSnd > Config.atomic_sets_locked_functions_limit then (
         finalCallsPairs := CallsPairSet.add (pFst, SSet.empty) !finalCallsPairs ;
         false )
@@ -134,31 +136,30 @@ let update_astate_el_after_calls (astateEl : tElement) : tElement =
 
 
 let apply_call ~(fName : string) : t -> t =
-  let mapper (astateEl : tElement) : tElement =
+  let mapper (astateEl : t_element) : t_element =
     let calls : SSet.t = SSet.add fName astateEl.calls
     and callsPairs : CallsPairLockSet.t =
       CallsPairLockSet.map
-        (fun (((pFst, pSnd), lock) : callsPairLock) : callsPairLock ->
+        (fun (((pFst, pSnd), lock) : calls_pair_lock) : calls_pair_lock ->
           ((pFst, SSet.add fName pSnd), lock))
         astateEl.callsPairs
-    and allOccurrences : SSet.t list =
-      List.mapi astateEl.allOccurrences ~f:(fun (i : int) : (SSet.t -> SSet.t) ->
+    and allCalls : SSet.t list =
+      List.mapi astateEl.allCalls ~f:(fun (i : int) : (SSet.t -> SSet.t) ->
           if Int.equal i 0 then SSet.add fName else Fn.id)
     in
-    (* Update the calls and the calls pairs and the all occurrences. *)
-    update_astate_el_after_calls {astateEl with calls; callsPairs; allOccurrences}
+    update_astate_el_after_calls {astateEl with calls; callsPairs; allCalls}
   in
   TSet.map mapper
 
 
 let apply_locks (locksPaths : AccessPath.t list) : t -> t =
-  let mapper (astateEl : tElement) : tElement =
+  let mapper (astateEl : t_element) : t_element =
     let lockAppended : bool ref = ref false
     and locksPaths : AccessPath.t list = Guards.reveal_locks astateEl.guards locksPaths in
     let callsPairs : CallsPairLockSet.t =
       let fold (callsPairs : CallsPairLockSet.t) (path : AccessPath.t) : CallsPairLockSet.t =
         let found : bool ref = ref false in
-        let mapper ((p, lock) as pairLock : callsPairLock) : callsPairLock =
+        let mapper ((p, lock) as pairLock : calls_pair_lock) : calls_pair_lock =
           if AccessPath.equal path (Lock.path lock) then (
             found := true ;
             (p, Lock.lock lock) )
@@ -172,31 +173,31 @@ let apply_locks (locksPaths : AccessPath.t list) : t -> t =
       in
       List.fold locksPaths ~init:astateEl.callsPairs ~f:fold
     and calls : SSet.t = if !lockAppended then SSet.empty else astateEl.calls in
-    (* Clear the calls and update the calls pairs. *)
     {astateEl with calls; callsPairs}
   in
   TSet.map mapper
 
 
 let apply_unlocks (locksPaths : AccessPath.t list) : t -> t =
-  let mapper (astateEl : tElement) : tElement =
+  let mapper (astateEl : t_element) : t_element =
     let lockRemoved : bool ref = ref false
     and finalCallsPairs : CallsPairSet.t ref = ref astateEl.finalCallsPairs
     and locksPaths : AccessPath.t list = Guards.reveal_locks astateEl.guards locksPaths in
     let callsPairs : CallsPairLockSet.t =
-      let mapper ((p, lock) as pairLock : callsPairLock) : callsPairLock =
-        if List.mem locksPaths (Lock.path lock) ~equal:AccessPath.equal then (
-          let lock : Lock.t = Lock.unlock lock in
-          if not (Lock.is_locked lock) then (
-            lockRemoved := true ;
-            finalCallsPairs := CallsPairSet.add p !finalCallsPairs ) ;
-          (p, lock) )
-        else pairLock
+      let mapper ((p, lock) as pairLock : calls_pair_lock) : calls_pair_lock option =
+        let ((_, lock) as pairLock : calls_pair_lock) =
+          if List.mem locksPaths (Lock.path lock) ~equal:AccessPath.equal then (
+            let lock : Lock.t = Lock.unlock lock in
+            if not (Lock.is_locked lock) then (
+              lockRemoved := true ;
+              finalCallsPairs := CallsPairSet.add p !finalCallsPairs ) ;
+            (p, lock) )
+          else pairLock
+        in
+        if Lock.is_locked lock then Some pairLock else None
       in
-      let callsPairs : CallsPairLockSet.t = CallsPairLockSet.map mapper astateEl.callsPairs in
-      CallsPairLockSet.filter (Fn.compose Lock.is_locked snd) callsPairs
+      CallsPairLockSet.filter_map mapper astateEl.callsPairs
     and calls : SSet.t = if !lockRemoved then SSet.empty else astateEl.calls in
-    (* Clear the calls, update the calls pairs and the final calls pairs. *)
     {astateEl with calls; callsPairs; finalCallsPairs= !finalCallsPairs}
   in
   TSet.map mapper
@@ -205,14 +206,14 @@ let apply_unlocks (locksPaths : AccessPath.t list) : t -> t =
 let apply_guard_construct (guardPath : AccessPath.t) (locksPaths : AccessPath.t list)
     ~(acquire : bool) : t -> t =
   let add_guard : t -> t =
-    TSet.map (fun (astateEl : tElement) : tElement ->
+    TSet.map (fun (astateEl : t_element) : t_element ->
         {astateEl with guards= Guards.add guardPath locksPaths astateEl.guards})
   in
   if acquire then Fn.compose (apply_locks locksPaths) add_guard else add_guard
 
 
 let apply_guard_release (guardPath : AccessPath.t) : t -> t =
-  TSet.map (fun (astateEl : tElement) : tElement ->
+  TSet.map (fun (astateEl : t_element) : t_element ->
       {astateEl with guards= Guards.remove guardPath astateEl.guards})
 
 
@@ -221,15 +222,14 @@ let apply_guard_destroy (guardPath : AccessPath.t) : t -> t =
 
 
 let update_at_the_end_of_function : t -> t =
-  let mapper (astateEl : tElement) : tElement =
+  let mapper (astateEl : t_element) : t_element =
     let finalCallsPairs : CallsPairSet.t ref = ref astateEl.finalCallsPairs in
     CallsPairLockSet.iter
-      (fun ((p, _) : callsPairLock) : unit ->
+      (fun ((p, _) : calls_pair_lock) : unit ->
         finalCallsPairs := CallsPairSet.add p !finalCallsPairs)
       astateEl.callsPairs ;
     if not (SSet.is_empty astateEl.calls) then
       finalCallsPairs := CallsPairSet.add (astateEl.calls, SSet.empty) !finalCallsPairs ;
-    (* Clear the calls and the calls pairs, and update the final calls pairs. *)
     { astateEl with
       calls= SSet.empty
     ; callsPairs= CallsPairLockSet.empty
@@ -260,7 +260,8 @@ let widen ~(prev : t) ~(next : t) ~(num_iters : int) : t =
 (* ************************************ Summary ************************************************* *)
 
 module Summary = struct
-  type t = {atomicFunctions: SSSet.t; allOccurrences: SSet.t list} [@@deriving compare, equal]
+  type t = {mutable atomicFunctions: SSSet.t; mutable allCalls: SSet.t list}
+  [@@deriving compare, equal]
 
   let pp (fmt : F.formatter) (summary : t) : unit =
     F.pp_print_string fmt "\n" ;
@@ -274,39 +275,39 @@ module Summary = struct
     F.pp_print_string fmt "atomicFunctions: " ;
     SSSet.iter print_atomic_functions summary.atomicFunctions ;
     F.pp_print_string fmt "\n" ;
-    (* allOccurrences *)
-    let print_all_occurrences (i : int) (allOccurrences : SSet.t) : unit =
-      F.fprintf fmt "\t%i: {%s};\n" i (String.concat (SSet.elements allOccurrences) ~sep:", ")
+    (* allCalls *)
+    let print_all_calls (i : int) (allCalls : SSet.t) : unit =
+      F.fprintf fmt "\t%i: {%s};\n" i (String.concat (SSet.elements allCalls) ~sep:", ")
     in
-    F.pp_print_string fmt "allOccurrences:\n{\n" ;
-    List.iteri summary.allOccurrences ~f:print_all_occurrences ;
+    F.pp_print_string fmt "allCalls:\n{\n" ;
+    List.iteri summary.allCalls ~f:print_all_calls ;
     F.pp_print_string fmt "}\n" ;
     F.pp_print_string fmt "\n"
 
 
   let create (astate : astate) : t =
-    (* Derivates atomic functions and all occurrences from the final calls pairs of elements of the
+    (* Derivates atomic functions and all calls from the final calls pairs of elements of the
        abstract state. *)
-    let atomicFunctions : SSSet.t ref = ref SSSet.empty
-    and allOccurrences : SSet.t list ref = ref [] in
-    let iterator (astateEl : tElement) : unit =
-      let iterator ((_, pSnd) : callsPair) : unit =
-        if not (SSet.is_empty pSnd) then atomicFunctions := SSSet.add pSnd !atomicFunctions
-      in
-      CallsPairSet.iter iterator astateEl.finalCallsPairs ;
-      let iterator (i : int) (occurrences : SSet.t) : unit =
-        allOccurrences :=
-          match List.nth !allOccurrences i with
+    let summary : t = {atomicFunctions= SSSet.empty; allCalls: SSet.t list = []} in
+    let iterator (astateEl : t_element) : unit =
+      CallsPairSet.iter
+        (fun ((_, pSnd) : calls_pair) : unit ->
+          if not (SSet.is_empty pSnd) then
+            summary.atomicFunctions <- SSSet.add pSnd summary.atomicFunctions)
+        astateEl.finalCallsPairs ;
+      let iterator (i : int) (calls : SSet.t) : unit =
+        summary.allCalls <-
+          ( match List.nth summary.allCalls i with
           | Some (_ : SSet.t) ->
-              List.mapi !allOccurrences ~f:(fun (j : int) : (SSet.t -> SSet.t) ->
-                  if Int.equal i j then SSet.union occurrences else Fn.id)
+              List.mapi summary.allCalls ~f:(fun (j : int) : (SSet.t -> SSet.t) ->
+                  if Int.equal i j then SSet.union calls else Fn.id)
           | None ->
-              if SSet.is_empty occurrences then !allOccurrences else !allOccurrences @ [occurrences]
+              if SSet.is_empty calls then summary.allCalls else summary.allCalls @ [calls] )
       in
-      List.iteri astateEl.allOccurrences ~f:iterator
+      List.iteri astateEl.allCalls ~f:iterator
     in
     TSet.iter iterator astate ;
-    {atomicFunctions= !atomicFunctions; allOccurrences= !allOccurrences}
+    summary
 
 
   let print_atomic_sets (summary : t) ~(fName : string) (oc : Out_channel.t) : int * int =
@@ -328,34 +329,32 @@ module Summary = struct
 end
 
 let apply_summary (summary : Summary.t) : t -> t =
-  (* Adds all occurrences from a given summary to the calls pairs and to the calls of each element
-     of the abstract state. And merges all occurrences from a given summary with the all occurrences
+  (* Adds all calls from a given summary to the calls pairs and to the calls of each element
+     of the abstract state. And merges all calls from a given summary with the all calls
      of each element of the abstract state. *)
-  let mapper (astateEl : tElement) : tElement =
-    let allOccurrences : SSet.t list ref = ref astateEl.allOccurrences
-    and joinedAllOccurrences : SSet.t ref = ref SSet.empty in
-    let iterator (i : int) (occurrences : SSet.t) : unit =
+  let mapper (astateEl : t_element) : t_element =
+    let allCalls : SSet.t list ref = ref astateEl.allCalls
+    and joinedAllCalls : SSet.t ref = ref SSet.empty in
+    let iterator (i : int) (calls : SSet.t) : unit =
       ( if i + 1 < Config.atomic_sets_functions_depth_limit then
-        allOccurrences :=
-          match List.nth !allOccurrences (i + 1) with
+        allCalls :=
+          match List.nth !allCalls (i + 1) with
           | Some (_ : SSet.t) ->
-              List.mapi !allOccurrences ~f:(fun (j : int) : (SSet.t -> SSet.t) ->
-                  if Int.equal (i + 1) j then SSet.union occurrences else Fn.id)
+              List.mapi !allCalls ~f:(fun (j : int) : (SSet.t -> SSet.t) ->
+                  if Int.equal (i + 1) j then SSet.union calls else Fn.id)
           | None ->
-              if SSet.is_empty occurrences then !allOccurrences else !allOccurrences @ [occurrences]
-      ) ;
+              if SSet.is_empty calls then !allCalls else !allCalls @ [calls] ) ;
       if i < Config.atomic_sets_functions_depth_limit then
-        joinedAllOccurrences := SSet.union !joinedAllOccurrences occurrences
+        joinedAllCalls := SSet.union !joinedAllCalls calls
     in
-    List.iteri summary.allOccurrences ~f:iterator ;
-    let calls : SSet.t = SSet.union astateEl.calls !joinedAllOccurrences
+    List.iteri summary.allCalls ~f:iterator ;
+    let calls : SSet.t = SSet.union astateEl.calls !joinedAllCalls
     and callsPairs : CallsPairLockSet.t =
       CallsPairLockSet.map
-        (fun (((pFst, pSnd), lock) : callsPairLock) : callsPairLock ->
-          ((pFst, SSet.union pSnd !joinedAllOccurrences), lock))
+        (fun (((pFst, pSnd), lock) : calls_pair_lock) : calls_pair_lock ->
+          ((pFst, SSet.union pSnd !joinedAllCalls), lock))
         astateEl.callsPairs
     in
-    (* Update the calls and the calls pairs and the all occurrences. *)
-    update_astate_el_after_calls {astateEl with calls; callsPairs; allOccurrences= !allOccurrences}
+    update_astate_el_after_calls {astateEl with calls; callsPairs; allCalls= !allCalls}
   in
   TSet.map mapper
diff --git a/infer/src/atomicity/AtomicSetsDomain.mli b/infer/src/atomicity/AtomicSetsDomain.mli
index da6b3cd54ab..8dc34faa791 100644
--- a/infer/src/atomicity/AtomicSetsDomain.mli
+++ b/infer/src/atomicity/AtomicSetsDomain.mli
@@ -7,8 +7,7 @@ module F = Format
 
 (* ************************************ Astate ************************************************** *)
 
-(** An abstract state of a function. *)
-type t [@@deriving compare, equal]
+include PrettyPrintable.PrintableEquatableOrderedType
 
 (** An alias for the type 't'. *)
 type astate = t [@@deriving compare, equal]
@@ -43,10 +42,7 @@ val update_at_the_end_of_function : t -> t
 
 (** A module that encapsulates a summary of a function. *)
 module Summary : sig
-  (** A summary of a function. *)
-  type t [@@deriving compare, equal]
-
-  include PrettyPrintable.PrintableType with type t := t
+  include PrettyPrintable.PrintableEquatableOrderedType
 
   val create : astate -> t
   (** Converts an abstract state to a summary. *)
diff --git a/infer/src/atomicity/AtomicityUtils.ml b/infer/src/atomicity/AtomicityUtils.ml
index d39fdd534bc..5e2ec5bb25d 100644
--- a/infer/src/atomicity/AtomicityUtils.ml
+++ b/infer/src/atomicity/AtomicityUtils.ml
@@ -43,7 +43,7 @@ module Lock = struct
       else if is_top lock then F.pp_print_string fmt SpecialChars.down_tack
       else F.pp_print_int fmt level
     in
-    F.fprintf fmt "%a (%a): " AccessPath.pp path pp_level lock
+    F.fprintf fmt "%a (%a)" AccessPath.pp path pp_level lock
 
 
   let lock ((path, level) as lock : t) : t = if is_top lock then lock else (path, level + 1)
@@ -63,8 +63,7 @@ module Guards = struct
 
   type t = AccessPath.t list GuardMap.t [@@deriving compare, equal]
 
-  let pp (fmt : F.formatter) (guards : t) : unit =
-    F.pp_print_string fmt "\t{\n" ;
+  let pp (fmt : F.formatter) : t -> unit =
     let print_guards (guard : AccessPath.t) : AccessPath.t list -> unit =
       let pp_locks (fmt : F.formatter) (locks : AccessPath.t list) : unit =
         let lastLock : AccessPath.t option = List.last locks in
@@ -76,8 +75,7 @@ module Guards = struct
       in
       F.fprintf fmt "\t\t%a: {%a};\n" AccessPath.pp guard pp_locks
     in
-    GuardMap.iter print_guards guards ;
-    F.pp_print_string fmt "\t};\n"
+    GuardMap.iter print_guards
 
 
   let empty : t = GuardMap.empty
@@ -98,9 +96,7 @@ end
 
 (* ************************************ Constants *********************************************** *)
 
-let inferDir : string = CommandLineOption.init_work_dir ^ "/infer-atomicity-out"
-
-let atomicSetsFile : string = inferDir ^ "/atomic-sets"
+let atomicSetsFile : string = CommandLineOption.init_work_dir ^ "/atomic-sets"
 
 let fileCommentChar : char = '#'
 
diff --git a/infer/src/atomicity/AtomicityUtils.mli b/infer/src/atomicity/AtomicityUtils.mli
index e759f97c653..e7bdc8a26d4 100644
--- a/infer/src/atomicity/AtomicityUtils.mli
+++ b/infer/src/atomicity/AtomicityUtils.mli
@@ -14,10 +14,7 @@ module SSet : module type of Set.Make (String)
 (** A module that represents a lock's access path with the number of times the lock has been
     acquired. *)
 module Lock : sig
-  (** A representation of a lock. *)
-  type t [@@deriving compare, equal]
-
-  include PrettyPrintable.PrintableType with type t := t
+  include PrettyPrintable.PrintableEquatableOrderedType
 
   val lock : t -> t
   (** Increases the number of times the lock has been acquired. *)
@@ -37,10 +34,7 @@ end
 
 (** A module that represents associations between lock guards and locks. *)
 module Guards : sig
-  (** A representation of associations between lock guards and locks. *)
-  type t [@@deriving compare, equal]
-
-  include PrettyPrintable.PrintableType with type t := t
+  include PrettyPrintable.PrintableEquatableOrderedType
 
   val empty : t
   (** Creates an empty module. *)
@@ -60,9 +54,6 @@ end
 
 (* ************************************ Constants *********************************************** *)
 
-val inferDir : string
-(** The Infer work directory. *)
-
 val atomicSetsFile : string
 (** A file for storing atomic sets. *)
 
diff --git a/infer/src/atomicity/AtomicityViolations.ml b/infer/src/atomicity/AtomicityViolations.ml
index 914b7f43913..541dcafda46 100644
--- a/infer/src/atomicity/AtomicityViolations.ml
+++ b/infer/src/atomicity/AtomicityViolations.ml
@@ -111,12 +111,36 @@ let analyse_procedure (analysis_data : Domain.Summary.t InterproceduralAnalysis.
         F.fprintf fmt "\n\nFunction: %a\n%a%a\n\n" Procname.pp pName Domain.pp post
           Domain.Summary.pp summary ;
         L.debug Capture Verbose "%s" (F.flush_str_formatter ()) ;
-        (* Report atomicity violations. *)
-        Domain.report_atomicity_violations post ~f:(fun (loc : Location.t) ~(msg : string) : unit ->
-            Reporting.log_issue analysis_data.proc_desc analysis_data.err_log ~loc
-              AtomicityViolations IssueType.atomicity_violation msg) ;
         Some summary
     | None ->
         L.die InternalError
           "The detection of atomicity violations failed to compute a post for '%a'." Procname.pp
           pName
+
+
+let report_atomicity_violations (analysis_data : Domain.Summary.t InterproceduralAnalysis.file_t) :
+    IssueLog.t =
+  let summaries : (Procname.t * Domain.Summary.t) list =
+    let mapper (pName : Procname.t) : (Procname.t * Domain.Summary.t) option =
+      match analysis_data.analyze_file_dependency pName with
+      | Some ((_ : Procdesc.t), (summary : Domain.Summary.t)) ->
+          Some (pName, summary)
+      | None ->
+          None
+    in
+    List.filter_map ~f:mapper analysis_data.procedures
+  in
+  let fold (issueLog : IssueLog.t) ((pName : Procname.t), (summary : Domain.Summary.t)) : IssueLog.t
+      =
+    if not (Domain.Summary.is_top_level_fun pName summaries) then issueLog
+    else
+      (* Report atomicity violations. *)
+      let report (loc : Location.t) ~(msg : string) (issueType : IssueType.t)
+          (issueLog : IssueLog.t) : IssueLog.t =
+        Reporting.log_issue_external pName ~issue_log:issueLog ~loc
+          ~ltr:[Errlog.make_trace_element 0 loc msg []]
+          AtomicityViolations issueType msg
+      in
+      Domain.Summary.report_atomicity_violations summary issueLog ~f:report
+  in
+  List.fold summaries ~init:IssueLog.empty ~f:fold
diff --git a/infer/src/atomicity/AtomicityViolations.mli b/infer/src/atomicity/AtomicityViolations.mli
index 846748581ec..5b7defcd247 100644
--- a/infer/src/atomicity/AtomicityViolations.mli
+++ b/infer/src/atomicity/AtomicityViolations.mli
@@ -8,3 +8,7 @@ module Domain = AtomicityViolationsDomain
 val analyse_procedure : Domain.Summary.t InterproceduralAnalysis.t -> Domain.Summary.t option
 (** An atomicity violations detection entry point. Produces a summary for a given function. Should
     be invoked for each function in the analysed program. Reports atomicity violations. *)
+
+val report_atomicity_violations : Domain.Summary.t InterproceduralAnalysis.file_t -> IssueLog.t
+(** Should be invoked after the atomicity violations detection of all functions in the analysed
+    program. Reports atomicity violations from summaries from all analysed functions. *)
diff --git a/infer/src/atomicity/AtomicityViolationsDomain.ml b/infer/src/atomicity/AtomicityViolationsDomain.ml
index cf14836ee2d..f4c1ec9dd0d 100644
--- a/infer/src/atomicity/AtomicityViolationsDomain.ml
+++ b/infer/src/atomicity/AtomicityViolationsDomain.ml
@@ -11,35 +11,119 @@ module Set = Caml.Set
 (* ************************************ Types *************************************************** *)
 
 (** A pair of atomic functions. *)
-type atomicPair = string * string [@@deriving compare, equal]
-
-(** A pair of atomic functions with its location. *)
-type atomicPairLoc = {pair: atomicPair; line: int; col: int; file: string}
-[@@deriving compare, equal]
+type atomic_pair = string * string [@@deriving compare, equal]
 
 (** A pair of atomic functions with a lock. *)
-type atomicPairLock = atomicPair * Lock.t [@@deriving compare, equal]
+type atomic_pair_lock = atomic_pair * Lock.t [@@deriving compare, equal]
 
 (* ************************************ Constants *********************************************** *)
 
 (** An empty pair of atomic functions. *)
-let emptyAtomicPair : atomicPair = ("", "")
+let emptyAtomicPair : atomic_pair = ("", "")
 
 (* ************************************ Modules ************************************************* *)
 
 (** A set of pairs of atomic functions. *)
 module AtomicPairSet = Set.Make (struct
-  type t = atomicPair [@@deriving compare, equal]
+  type t = atomic_pair [@@deriving compare, equal]
 end)
 
-(** A set of pairs of atomic functions with their locations. *)
-module AtomicPairLocSet = Set.Make (struct
-  type t = atomicPairLoc [@@deriving compare, equal]
-end)
+(** A module that represents atomicity violations to be reported. *)
+module Violations : sig
+  include PrettyPrintable.PrintableEquatableOrderedType
+
+  (** A severity of an atomicity violation to be reported. *)
+  type violation_severity = private
+    | Warning  (** WARNING severity - used for local atomicity violations. *)
+    | Error  (** ERROR severity - used for real (global) atomicity violations. *)
+  [@@deriving compare, equal]
+
+  val empty : t
+  (** Creates an empty module. *)
+
+  val is_empty : t -> bool
+  (** Checks whether there are any violations to be reported. *)
+
+  val add : atomic_pair -> Location.t -> t -> t
+  (** Adds a new violation to be reported. *)
+
+  val union : t -> t -> t
+  (** Makes an union of atomicity violations to be reported. *)
+
+  val fold : f:(atomic_pair * Location.t * violation_severity -> 'a -> 'a) -> t -> 'a -> 'a
+  (** [fold ~f:f s a] computes (f xN ... (f x2 (f x1 a))...), where x1 ... xN are the elements of s,
+      in increasing order. *)
+
+  val make_all_warnings : t -> t
+  (** Labels all atomicity violations to be reported as warnings. *)
+
+  val severity_to_issue_type : violation_severity -> IssueType.t
+  (** Converts the severity of a violation to IssueType. *)
+end = struct
+  type violation_severity = Warning | Error [@@deriving compare, equal]
+
+  (** A structure that represents a single atomicity violation to be reported. *)
+  type violation =
+    {pair: atomic_pair; line: int; col: int; file: string; severity: violation_severity}
+  [@@deriving compare, equal]
+
+  (** A set of atomicity violations to be reported. *)
+  module ViolationSet = Set.Make (struct
+    type t = violation [@@deriving compare, equal]
+  end)
+
+  type t = ViolationSet.t [@@deriving compare, equal]
+
+  let pp (fmt : F.formatter) (violations : t) : unit =
+    let lastViolation : violation option = ViolationSet.max_elt_opt violations in
+    let print_violation (violation : violation) : unit =
+      let pp_severity (fmt : F.formatter) : violation_severity -> unit = function
+        | Warning ->
+            F.pp_print_string fmt "WARNING"
+        | Error ->
+            F.pp_print_string fmt "ERROR"
+      in
+      F.fprintf fmt "%s:%i:%i: %a -> (%s, %s)" violation.file violation.line violation.col
+        pp_severity violation.severity (fst violation.pair) (snd violation.pair) ;
+      if not (equal_violation violation (Option.value_exn lastViolation)) then
+        F.pp_print_string fmt " | "
+    in
+    ViolationSet.iter print_violation violations
+
+
+  let empty : t = ViolationSet.empty
+
+  let is_empty : t -> bool = ViolationSet.is_empty
+
+  let add (pair : atomic_pair) (loc : Location.t) : t -> t =
+    ViolationSet.add
+      {pair; line= loc.line; col= loc.col; file= SourceFile.to_abs_path loc.file; severity= Error}
+
+
+  let union : t -> t -> t = ViolationSet.union
+
+  let fold ~(f : atomic_pair * Location.t * violation_severity -> 'a -> 'a) : t -> 'a -> 'a =
+    ViolationSet.fold (fun (violation : violation) : ('a -> 'a) ->
+        let loc : Location.t =
+          {line= violation.line; col= violation.col; file= SourceFile.from_abs_path violation.file}
+        in
+        f (violation.pair, loc, violation.severity))
+
+
+  let make_all_warnings : t -> t =
+    ViolationSet.map (fun (violation : violation) : violation -> {violation with severity= Warning})
+
+
+  let severity_to_issue_type : violation_severity -> IssueType.t = function
+    | Warning ->
+        IssueType.atomicity_violation_warning
+    | Error ->
+        IssueType.atomicity_violation_error
+end
 
 (** A set of pairs of atomic functions with locks. *)
 module AtomicPairLockSet = Set.Make (struct
-  type t = atomicPairLock [@@deriving compare, equal]
+  type t = atomic_pair_lock [@@deriving compare, equal]
 end)
 
 (* ************************************ Classes ************************************************* *)
@@ -100,22 +184,19 @@ class atomic_pairs =
         In_channel.close ic )
 
     (** Checks whether an atomic pair is violating atomicity. *)
-    method check_violating_atomicity ?(checkFirstEmpty : bool = false) ((_, pSnd) as p : atomicPair)
-        ~(atomicityViolations : AtomicPairLocSet.t ref) ~(lockedLastPairs : AtomicPairLockSet.t)
-        (loc : Location.t) : unit =
+    method check_violating_atomicity ?(checkFirstEmpty : bool = false)
+        ((_, pSnd) as p : atomic_pair) ~(violations : Violations.t ref)
+        ~(lockedLastPairs : AtomicPairLockSet.t) (loc : Location.t) : unit =
       self#init ;
-      let check (p : atomicPair) : unit =
-        let is_pair_locked (p : atomicPair) : bool =
-          AtomicPairLockSet.fold
-            (fun ((((_, pSnd') as p'), _) : atomicPairLock) : (bool -> bool) ->
-              ( || ) (equal_atomicPair p' p || (checkFirstEmpty && equal_atomicPair ("", pSnd') p)))
-            lockedLastPairs false
-        and make_atomic_pair_loc (p : atomicPair) (loc : Location.t) : atomicPairLoc =
-          {pair= p; line= loc.line; col= loc.col; file= SourceFile.to_abs_path loc.file}
+      let check (p : atomic_pair) : unit =
+        let is_pair_locked (p : atomic_pair) : bool =
+          let fold ((((_, pSnd') as p'), _) : atomic_pair_lock) : bool -> bool =
+            ( || ) (equal_atomic_pair p' p || (checkFirstEmpty && equal_atomic_pair ("", pSnd') p))
+          in
+          AtomicPairLockSet.fold fold lockedLastPairs false
         in
         if AtomicPairSet.mem p pairs && not (is_pair_locked p) then
-          atomicityViolations :=
-            AtomicPairLocSet.add (make_atomic_pair_loc p loc) !atomicityViolations
+          violations := Violations.add p loc !violations
       in
       check p ;
       if checkFirstEmpty then check ("", pSnd)
@@ -127,18 +208,19 @@ let atomicPairs : atomic_pairs = new atomic_pairs
 (* ************************************ Astate ************************************************** *)
 
 (** An element of an abstract state. *)
-type tElement =
+type t_element =
   { firstCall: string
-  ; lastPair: atomicPair
+  ; lastPair: atomic_pair
   ; nestedLastCalls: SSet.t
-  ; atomicityViolations: AtomicPairLocSet.t
+  ; violations: Violations.t
   ; lockedLastPairs: AtomicPairLockSet.t
-  ; guards: Guards.t }
+  ; guards: Guards.t
+  ; allCalls: SSet.t }
 [@@deriving compare, equal]
 
 (** A set of types tElement is an abstract state. *)
 module TSet = Set.Make (struct
-  type t = tElement [@@deriving compare, equal]
+  type t = t_element [@@deriving compare, equal]
 end)
 
 type t = TSet.t [@@deriving compare, equal]
@@ -155,14 +237,15 @@ let initial : t =
     { firstCall= ""
     ; lastPair= emptyAtomicPair
     ; nestedLastCalls= SSet.empty
-    ; atomicityViolations= AtomicPairLocSet.empty
+    ; violations= Violations.empty
     ; lockedLastPairs= AtomicPairLockSet.empty
-    ; guards= Guards.empty }
+    ; guards= Guards.empty
+    ; allCalls= SSet.empty }
 
 
 let pp (fmt : F.formatter) (astate : t) : unit =
   F.pp_print_string fmt "\n" ;
-  let iterator (astateEl : tElement) : unit =
+  let iterator (astateEl : t_element) : unit =
     F.pp_print_string fmt "{\n" ;
     (* firstCall *)
     F.fprintf fmt "\t%s;\n" astateEl.firstCall ;
@@ -171,31 +254,23 @@ let pp (fmt : F.formatter) (astate : t) : unit =
     (* nestedLastCalls *)
     F.fprintf fmt "\t{%s};\n" (String.concat (SSet.elements astateEl.nestedLastCalls) ~sep:", ") ;
     (* atomicityViolations *)
-    F.pp_print_string fmt "\t" ;
-    let lastAtomicityViolationsPair : atomicPairLoc option =
-      AtomicPairLocSet.max_elt_opt astateEl.atomicityViolations
-    in
-    let print_atomicity_violations_pair (p : atomicPairLoc) : unit =
-      F.fprintf fmt "%s:%i:%i -> (%s, %s)" p.file p.line p.col (fst p.pair) (snd p.pair) ;
-      if not (equal_atomicPairLoc p (Option.value_exn lastAtomicityViolationsPair)) then
-        F.pp_print_string fmt " | "
-    in
-    AtomicPairLocSet.iter print_atomicity_violations_pair astateEl.atomicityViolations ;
-    F.pp_print_string fmt ";\n" ;
+    F.fprintf fmt "\t%a;\n" Violations.pp astateEl.violations ;
     (* lockedLastPairs *)
     F.pp_print_string fmt "\t" ;
-    let lastLockedLastPair : atomicPairLock option =
+    let lastLockedLastPair : atomic_pair_lock option =
       AtomicPairLockSet.max_elt_opt astateEl.lockedLastPairs
     in
-    let print_locked_last_pair (((pFst, pSnd), lock) as lockedLastPair : atomicPairLock) : unit =
-      F.fprintf fmt "%a(%s, %s)" Lock.pp lock pFst pSnd ;
-      if not (equal_atomicPairLock lockedLastPair (Option.value_exn lastLockedLastPair)) then
+    let print_locked_last_pair (((pFst, pSnd), lock) as lockedLastPair : atomic_pair_lock) : unit =
+      F.fprintf fmt "%a: (%s, %s)" Lock.pp lock pFst pSnd ;
+      if not (equal_atomic_pair_lock lockedLastPair (Option.value_exn lastLockedLastPair)) then
         F.pp_print_string fmt " | "
     in
     AtomicPairLockSet.iter print_locked_last_pair astateEl.lockedLastPairs ;
     F.pp_print_string fmt ";\n" ;
     (* guards *)
-    F.fprintf fmt "%a" Guards.pp astateEl.guards ;
+    F.fprintf fmt "\t{\n%a\t};\n" Guards.pp astateEl.guards ;
+    (* allCalls *)
+    F.fprintf fmt "\t{%s};\n" (String.concat (SSet.elements astateEl.allCalls) ~sep:", ") ;
     F.pp_print_string fmt "}\n"
   in
   TSet.iter iterator astate ;
@@ -203,53 +278,52 @@ let pp (fmt : F.formatter) (astate : t) : unit =
 
 
 let apply_call ~(fName : string) (loc : Location.t) : t -> t =
-  let mapper (astateEl : tElement) : tElement =
-    let atomic_pair_push ((_, pSnd) : atomicPair) : string -> atomicPair = Tuple2.create pSnd in
+  let mapper (astateEl : t_element) : t_element =
+    let atomic_pair_push ((_, pSnd) : atomic_pair) : string -> atomic_pair = Tuple2.create pSnd in
     let firstCall : string =
       if String.is_empty astateEl.firstCall then fName else astateEl.firstCall
-    and lastPair : atomicPair = atomic_pair_push astateEl.lastPair fName
-    and atomicityViolations : AtomicPairLocSet.t ref = ref astateEl.atomicityViolations
+    and lastPair : atomic_pair = atomic_pair_push astateEl.lastPair fName
+    and violations : Violations.t ref = ref astateEl.violations
     and lockedLastPairs : AtomicPairLockSet.t =
       (* Updates pairs of atomic functions. *)
       AtomicPairLockSet.map
-        (fun ((p, lock) : atomicPairLock) : atomicPairLock -> (atomic_pair_push p fName, lock))
+        (fun ((p, lock) : atomic_pair_lock) : atomic_pair_lock -> (atomic_pair_push p fName, lock))
         astateEl.lockedLastPairs
-    in
+    and allCalls : SSet.t = SSet.add fName astateEl.allCalls in
     (* Check whether the last pair is violating atomicity. *)
-    atomicPairs#check_violating_atomicity lastPair ~atomicityViolations ~lockedLastPairs loc
+    atomicPairs#check_violating_atomicity lastPair ~violations ~lockedLastPairs loc
       ~checkFirstEmpty:true ;
     let iterator (lastCall : string) : unit =
-      let p : atomicPair = (lastCall, fName) in
+      let p : atomic_pair = (lastCall, fName) in
       let lockedLastPairs : AtomicPairLockSet.t =
         AtomicPairLockSet.map
-          (fun ((p', lock) : atomicPairLock) : atomicPairLock ->
+          (fun ((p', lock) : atomic_pair_lock) : atomic_pair_lock ->
             ((if String.is_empty (fst p') then p' else p), lock))
           lockedLastPairs
       in
       (* Check whether each pair begining with the nested last call and ending with the current
          function call is violating atomicity. *)
-      atomicPairs#check_violating_atomicity p ~atomicityViolations ~lockedLastPairs loc
+      atomicPairs#check_violating_atomicity p ~violations ~lockedLastPairs loc
     in
     SSet.iter iterator astateEl.nestedLastCalls ;
-    (* Update the first call, the last pair, the atomicity violations, the locked last pairs, and
-       clear the nested last calls. *)
     { astateEl with
       firstCall
     ; lastPair
     ; nestedLastCalls= SSet.empty
-    ; atomicityViolations= !atomicityViolations
-    ; lockedLastPairs }
+    ; violations= !violations
+    ; lockedLastPairs
+    ; allCalls }
   in
   TSet.map mapper
 
 
 let apply_locks (locksPaths : AccessPath.t list) : t -> t =
-  let mapper (astateEl : tElement) : tElement =
+  let mapper (astateEl : t_element) : t_element =
     let locksPaths : AccessPath.t list = Guards.reveal_locks astateEl.guards locksPaths in
     let lockedLastPairs : AtomicPairLockSet.t =
       let fold (lockedLastPairs : AtomicPairLockSet.t) (path : AccessPath.t) : AtomicPairLockSet.t =
         let found : bool ref = ref false in
-        let mapper ((p, lock) as pairLock : atomicPairLock) : atomicPairLock =
+        let mapper ((p, lock) as pairLock : atomic_pair_lock) : atomic_pair_lock =
           if AccessPath.equal path (Lock.path lock) then (
             found := true ;
             (p, Lock.lock lock) )
@@ -267,17 +341,17 @@ let apply_locks (locksPaths : AccessPath.t list) : t -> t =
 
 
 let apply_unlocks (locksPaths : AccessPath.t list) : t -> t =
-  let mapper (astateEl : tElement) : tElement =
+  let mapper (astateEl : t_element) : t_element =
     let locksPaths : AccessPath.t list = Guards.reveal_locks astateEl.guards locksPaths in
     let lockedLastPairs : AtomicPairLockSet.t =
-      let mapper ((p, lock) as pairLock : atomicPairLock) : atomicPairLock =
-        if List.mem locksPaths (Lock.path lock) ~equal:AccessPath.equal then (p, Lock.unlock lock)
-        else pairLock
-      in
-      let lockedLastPairs : AtomicPairLockSet.t =
-        AtomicPairLockSet.map mapper astateEl.lockedLastPairs
+      let mapper ((p, lock) as pairLock : atomic_pair_lock) : atomic_pair_lock option =
+        let ((_, lock) as pairLock : atomic_pair_lock) =
+          if List.mem locksPaths (Lock.path lock) ~equal:AccessPath.equal then (p, Lock.unlock lock)
+          else pairLock
+        in
+        if Lock.is_locked lock then Some pairLock else None
       in
-      AtomicPairLockSet.filter (Fn.compose Lock.is_locked snd) lockedLastPairs
+      AtomicPairLockSet.filter_map mapper astateEl.lockedLastPairs
     in
     {astateEl with lockedLastPairs}
   in
@@ -287,14 +361,14 @@ let apply_unlocks (locksPaths : AccessPath.t list) : t -> t =
 let apply_guard_construct (guardPath : AccessPath.t) (locksPaths : AccessPath.t list)
     ~(acquire : bool) : t -> t =
   let add_guard : t -> t =
-    TSet.map (fun (astateEl : tElement) : tElement ->
+    TSet.map (fun (astateEl : t_element) : t_element ->
         {astateEl with guards= Guards.add guardPath locksPaths astateEl.guards})
   in
   if acquire then Fn.compose (apply_locks locksPaths) add_guard else add_guard
 
 
 let apply_guard_release (guardPath : AccessPath.t) : t -> t =
-  TSet.map (fun (astateEl : tElement) : tElement ->
+  TSet.map (fun (astateEl : t_element) : t_element ->
       {astateEl with guards= Guards.remove guardPath astateEl.guards})
 
 
@@ -302,28 +376,6 @@ let apply_guard_destroy (guardPath : AccessPath.t) : t -> t =
   Fn.compose (apply_guard_release guardPath) (apply_unlocks [guardPath])
 
 
-let report_atomicity_violations ~(f : Location.t -> msg:string -> unit) : t -> unit =
-  (* Report atomicity violations from atomicity violations stored in the abstract state. *)
-  let iterator (astateEl : tElement) : unit =
-    let iterator (p : atomicPairLoc) : unit =
-      let (fst, snd) : atomicPair = p.pair in
-      if (not (String.is_empty fst)) || not (String.is_empty snd) then
-        let loc : Location.t = {line= p.line; col= p.col; file= SourceFile.from_abs_path p.file}
-        and msg : string =
-          if (not (String.is_empty fst)) && not (String.is_empty snd) then
-            F.asprintf "Atomicity Violation! - Functions '%s' and '%s' should be called atomically."
-              fst snd
-          else
-            F.asprintf "Atomicity Violation! - Function '%s' should be called atomically."
-              (if String.is_empty fst then snd else fst)
-        in
-        f loc ~msg
-    in
-    AtomicPairLocSet.iter iterator astateEl.atomicityViolations
-  in
-  TSet.iter iterator
-
-
 (* ************************************ Operators *********************************************** *)
 
 let leq ~(lhs : t) ~(rhs : t) : bool =
@@ -346,7 +398,12 @@ let widen ~(prev : t) ~(next : t) ~(num_iters : int) : t =
 (* ************************************ Summary ************************************************* *)
 
 module Summary = struct
-  type t = {firstCalls: SSet.t; lastCalls: SSet.t} [@@deriving compare, equal]
+  type t =
+    { mutable firstCalls: SSet.t
+    ; mutable lastCalls: SSet.t
+    ; mutable violations: Violations.t
+    ; mutable allCalls: SSet.t }
+  [@@deriving compare, equal]
 
   let pp (fmt : F.formatter) (summary : t) : unit =
     F.pp_print_string fmt "\n" ;
@@ -354,41 +411,92 @@ module Summary = struct
     F.fprintf fmt "firstCalls: {%s}\n" (String.concat (SSet.elements summary.firstCalls) ~sep:", ") ;
     (* lastCalls *)
     F.fprintf fmt "lastCalls: {%s}\n" (String.concat (SSet.elements summary.lastCalls) ~sep:", ") ;
+    (* violations *)
+    F.fprintf fmt "violations: %a\n" Violations.pp summary.violations ;
+    (* allCalls *)
+    F.fprintf fmt "allCalls: {%s}\n" (String.concat (SSet.elements summary.allCalls) ~sep:", ") ;
     F.pp_print_string fmt "\n"
 
 
   let create (astate : astate) : t =
     (* Derivates the first calls and the last calls from the first calls and from the last pairs of
        elements of the abstract state. *)
-    let firstCalls : SSet.t ref = ref SSet.empty and lastCalls : SSet.t ref = ref SSet.empty in
-    let iterator (astateEl : tElement) : unit =
+    let summary : t =
+      { firstCalls= SSet.empty
+      ; lastCalls= SSet.empty
+      ; violations= Violations.empty
+      ; allCalls= SSet.empty }
+    in
+    let iterator (astateEl : t_element) : unit =
       if not (String.is_empty astateEl.firstCall) then
-        firstCalls := SSet.add astateEl.firstCall !firstCalls ;
+        summary.firstCalls <- SSet.add astateEl.firstCall summary.firstCalls ;
       if not (String.is_empty (snd astateEl.lastPair)) then
-        lastCalls := SSet.add (snd astateEl.lastPair) !lastCalls
+        summary.lastCalls <- SSet.add (snd astateEl.lastPair) summary.lastCalls ;
+      summary.violations <- Violations.union astateEl.violations summary.violations ;
+      summary.allCalls <- SSet.union astateEl.allCalls summary.allCalls
     in
     TSet.iter iterator astate ;
-    {firstCalls= !firstCalls; lastCalls= !lastCalls}
+    summary
+
+
+  let is_top_level_fun (pName : Procname.t) : (Procname.t * t) list -> bool =
+    List.for_all ~f:(fun ((pName' : Procname.t), (summary : t)) : bool ->
+        Procname.equal pName' pName || not (SSet.mem (Procname.to_string pName) summary.allCalls))
+
+
+  let report_atomicity_violations
+      ~(f : Location.t -> msg:string -> IssueType.t -> IssueLog.t -> IssueLog.t) (summary : t) :
+      IssueLog.t -> IssueLog.t =
+    (* Report atomicity violations from atomicity violations stored in the summary. *)
+    let fold
+        (((fst, snd) : atomic_pair), (loc : Location.t), (severity : Violations.violation_severity))
+        (issueLog : IssueLog.t) : IssueLog.t =
+      if String.is_empty fst && String.is_empty snd then issueLog
+      else
+        let msg : string =
+          let warningMsg : string =
+            match severity with Warning -> " within a Current Function" | _ -> ""
+          in
+          if (not (String.is_empty fst)) && not (String.is_empty snd) then
+            F.asprintf
+              "Atomicity Violation%s! - Functions '%s' and '%s' should be called atomically."
+              warningMsg fst snd
+          else
+            F.asprintf "Atomicity Violation%s! - Function '%s' should be called atomically."
+              warningMsg
+              (if String.is_empty fst then snd else fst)
+        in
+        f loc ~msg (Violations.severity_to_issue_type severity) issueLog
+    in
+    Violations.fold ~f:fold summary.violations
 end
 
 let apply_summary (summary : Summary.t) (loc : Location.t) : t -> t =
   (* Add the last calls from a given summary to the nested last calls of the abstract state and
      check for atomicity violations with the first calls of a given summary. *)
-  if SSet.is_empty summary.firstCalls && SSet.is_empty summary.lastCalls then Fn.id
+  if
+    SSet.is_empty summary.firstCalls && SSet.is_empty summary.lastCalls
+    && Violations.is_empty summary.violations
+  then Fn.id
   else
-    let mapper (astateEl : tElement) : tElement =
-      let atomicityViolations : AtomicPairLocSet.t ref = ref astateEl.atomicityViolations
+    let mapper (astateEl : t_element) : t_element =
+      let violations : Violations.t ref =
+        let summaryViolations : Violations.t =
+          if AtomicPairLockSet.is_empty astateEl.lockedLastPairs then summary.violations
+          else Violations.make_all_warnings summary.violations
+        in
+        ref (Violations.union astateEl.violations summaryViolations)
       and lastCall : string = snd astateEl.lastPair in
       let iterator (firstCall : string) : unit =
-        let p : atomicPair = (lastCall, firstCall) in
+        let p : atomic_pair = (lastCall, firstCall) in
         let lockedLastPairs : AtomicPairLockSet.t =
           AtomicPairLockSet.map (Fn.compose (Tuple2.create p) snd) astateEl.lockedLastPairs
         in
         (* Check whether each pair begining with the last called function and ending witch the first
            call of a given summary is violating atomicity. *)
-        atomicPairs#check_violating_atomicity p ~atomicityViolations ~lockedLastPairs loc
+        atomicPairs#check_violating_atomicity p ~violations ~lockedLastPairs loc
       in
       SSet.iter iterator summary.firstCalls ;
-      {astateEl with nestedLastCalls= summary.lastCalls; atomicityViolations= !atomicityViolations}
+      {astateEl with nestedLastCalls= summary.lastCalls; violations= !violations}
     in
     TSet.map mapper
diff --git a/infer/src/atomicity/AtomicityViolationsDomain.mli b/infer/src/atomicity/AtomicityViolationsDomain.mli
index c541258c028..085a46d33cb 100644
--- a/infer/src/atomicity/AtomicityViolationsDomain.mli
+++ b/infer/src/atomicity/AtomicityViolationsDomain.mli
@@ -7,8 +7,7 @@ module F = Format
 
 (* ************************************ Astate ************************************************** *)
 
-(** An abstract state of a function. *)
-type t [@@deriving compare, equal]
+include PrettyPrintable.PrintableEquatableOrderedType
 
 (** An alias for the type 't'. *)
 type astate = t [@@deriving compare, equal]
@@ -36,20 +35,25 @@ val apply_guard_release : AccessPath.t -> t -> t
 val apply_guard_destroy : AccessPath.t -> t -> t
 (** Updates an abstract state on a lock guard destructor call. *)
 
-val report_atomicity_violations : f:(Location.t -> msg:string -> unit) -> t -> unit
-(** Reports atomicity violations from an abstract state using reporting function. *)
-
 (* ************************************ Summary ************************************************* *)
 
 (** A module that encapsulates a summary of a function. *)
 module Summary : sig
-  (** A summary of a function. *)
-  type t [@@deriving compare, equal]
-
-  include PrettyPrintable.PrintableType with type t := t
+  include PrettyPrintable.PrintableEquatableOrderedType
 
   val create : astate -> t
   (** Converts an abstract state to a summary. *)
+
+  val is_top_level_fun : Procname.t -> (Procname.t * t) list -> bool
+  (** Determines whether a given function is a top level function (using a list of all analysed
+      functions with their summaries). *)
+
+  val report_atomicity_violations :
+       f:(Location.t -> msg:string -> IssueType.t -> IssueLog.t -> IssueLog.t)
+    -> t
+    -> IssueLog.t
+    -> IssueLog.t
+  (** Reports atomicity violations from the summary using a reporting function. *)
 end
 
 val apply_summary : Summary.t -> Location.t -> t -> t
diff --git a/infer/src/backend/registerCheckers.ml b/infer/src/backend/registerCheckers.ml
index 27eef14df03..4637bfafaab 100644
--- a/infer/src/backend/registerCheckers.ml
+++ b/infer/src/backend/registerCheckers.ml
@@ -209,8 +209,11 @@ let all_checkers =
         (let checker : callback_fun =
            interprocedural Payloads.Fields.atomicity_violations
              AtomicityViolations.analyse_procedure
+         and checkerFile : callback_fun =
+           file AtomicityViolationsIssues Payloads.Fields.atomicity_violations
+             AtomicityViolations.report_atomicity_violations
          in
-         [(checker, Clang); (checker, Java)]) } ]
+         [(checker, Clang); (checker, Java); (checkerFile, Clang); (checkerFile, Java)]) } ]
 
 
 let get_active_checkers () =
diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml
index f2e5414002f..a72406ef4ad 100644
--- a/infer/src/base/IssueType.ml
+++ b/infer/src/base/IssueType.ml
@@ -991,13 +991,20 @@ let wrong_argument_number =
 
 let unreachable_cost_call ~kind = register_cost ~enabled:false ~kind "%s_UNREACHABLE_AT_EXIT"
 
-let atomicity_violation : t =
-  register ~id:"ATOMICITY_VIOLATION" ~enabled:true Error AtomicityViolations
+let atomicity_violation_error : t =
+  register ~id:"ATOMICITY_VIOLATION_ERROR" ~enabled:true Error AtomicityViolations
     ~hum:"Atomicity Violation"
     ~user_documentation:
       "See https://github.com/harmim/infer/wiki/Atomer:-Atomicity-Violations-Analyser."
 
 
+let atomicity_violation_warning : t =
+  register ~id:"ATOMICITY_VIOLATION_WARNING" ~enabled:true Warning AtomicityViolations
+    ~hum:"Atomicity Violation within a Function"
+    ~user_documentation:
+      "See https://github.com/harmim/infer/wiki/Atomer:-Atomicity-Violations-Analyser."
+
+
 (* register enabled cost issues *)
 let is_autoreleasepool_size_issue =
   let autoreleasepool_size_issues = ref IssueSet.empty in
diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli
index 53fb43cae8f..3a97717ec1a 100644
--- a/infer/src/base/IssueType.mli
+++ b/infer/src/base/IssueType.mli
@@ -358,4 +358,6 @@ val unreachable_cost_call : kind:CostKind.t -> t
 
 val is_autoreleasepool_size_issue : t -> bool
 
-val atomicity_violation : t
+val atomicity_violation_error : t
+
+val atomicity_violation_warning : t
diff --git a/infer/src/base/ResultsDirEntryName.ml b/infer/src/base/ResultsDirEntryName.ml
index 9196a765b6b..037ff7a0293 100644
--- a/infer/src/base/ResultsDirEntryName.ml
+++ b/infer/src/base/ResultsDirEntryName.ml
@@ -36,6 +36,7 @@ type id =
   | Temporary
   | TestDeterminatorReport
   | TestDeterminatorTempResults
+  | AtomicityViolationsIssues
 [@@deriving enumerate]
 
 type cleanup_action = Delete | Keep [@@deriving equal]
@@ -182,6 +183,11 @@ let of_id = function
       ; kind= Directory
       ; before_incremental_analysis= Delete
       ; before_caching_capture= Delete }
+  | AtomicityViolationsIssues ->
+      { rel_path= "atomicity_issues"
+      ; kind= IssuesDirectory
+      ; before_incremental_analysis= Delete
+      ; before_caching_capture= Delete }
 
 
 let path_of_entry ~results_dir {rel_path; _} = results_dir ^/ rel_path
diff --git a/infer/src/base/ResultsDirEntryName.mli b/infer/src/base/ResultsDirEntryName.mli
index 8305ba28f3e..7ea68545831 100644
--- a/infer/src/base/ResultsDirEntryName.mli
+++ b/infer/src/base/ResultsDirEntryName.mli
@@ -37,6 +37,8 @@ type id =
   | Temporary  (** directory containing temp files *)
   | TestDeterminatorReport  (** the report produced by the test determinator capture mode *)
   | TestDeterminatorTempResults  (** a directory *)
+  | AtomicityViolationsIssues
+      (** a directory of issues reported by the atomicity violations analysis *)
 
 val get_path : results_dir:string -> id -> string
 (** the absolute path for the given entry *)