[Inferbo] No need to check Bottom states

Summary:
`Bottom` is only useful for unreachable code detection, which is already handled.
Let's not check `Bottom` states.

Depends on D7289084

Reviewed By: skcho

Differential Revision: D7289153

fbshipit-source-id: 8333ce7

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -350,9 +350,11 @@ module Report = struct
           false
   end
 
-  let check_unreachable_code summary tenv node instr rem_instrs (mem, mem') =
+  let check_unreachable_code summary tenv node instr rem_instrs mem =
-    match (mem, mem') with
+    match mem with
-    | NonBottom _, Bottom -> (
+    | NonBottom _ ->
+        ()
+    | Bottom ->
       match instr with
       | Sil.Prune (_, _, _, (Ik_land_lor | Ik_bexp)) ->
           ()
@@ -370,9 +372,7 @@ module Report = struct
           let location = Sil.instr_get_loc instr in
           let desc = Errdesc.explain_unreachable_code_after location in
           let exn = Exceptions.Unreachable_code_after (desc, __POS__) in
-          Reporting.log_error summary ~loc:location exn )
+          Reporting.log_error summary ~loc:location exn
-    | _ ->
-        ()
 
 
   let check_binop_array_access
@@ -483,15 +483,15 @@ module Report = struct
       : Specs.summary -> extras ProcData.t -> CFG.node -> Sil.instr list -> Dom.Mem.astate
         -> PO.ConditionSet.t -> PO.ConditionSet.t =
    fun summary ({tenv} as pdata) node instrs mem cond_set ->
-    match instrs with
+    match (mem, instrs) with
-    | [] ->
+    | _, [] | Bottom, _ ->
         cond_set
-    | instr :: rem_instrs ->
+    | NonBottom _, instr :: rem_instrs ->
         let cond_set = check_instr pdata node instr mem cond_set in
-        let mem' = Analyzer.TransferFunctions.exec_instr mem pdata node instr in
+        let mem = Analyzer.TransferFunctions.exec_instr mem pdata node instr in
-        let () = check_unreachable_code summary tenv node instr rem_instrs (mem, mem') in
+        let () = check_unreachable_code summary tenv node instr rem_instrs mem in
-        print_debug_info instr mem' cond_set ;
+        print_debug_info instr mem cond_set ;
-        check_instrs summary pdata node rem_instrs mem' cond_set
+        check_instrs summary pdata node rem_instrs mem cond_set
 
 
   let check_node