From c6b222c75703126390c13efdbadc3493d2e1551c Mon Sep 17 00:00:00 2001
From: Mehdi Bouaziz <mbouaziz@fb.com>
Date: Mon, 28 Jan 2019 06:09:53 -0800
Subject: [PATCH] [inferbo] Always update summary

Summary:
In some rare cases, the CFG is broken, the analysis cannot reach the exit node and we won't update the summary for this procedure.
In this diff, the summary is gonna be updated with `Bottom` instead.

Reviewed By: skcho

Differential Revision: D13801731

fbshipit-source-id: 79d412429
---
 infer/src/bufferoverrun/bufferOverrunChecker.ml | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml
index 64420f8be..81b7e2d50 100644
--- a/infer/src/bufferoverrun/bufferOverrunChecker.ml
+++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml
@@ -659,14 +659,12 @@ let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_
       Report.check_proc summary proc_desc tenv integer_type_widths cfg inv_map
       |> Report.report_errors summary |> Report.forget_locs locals |> Report.for_summary
     in
-    let exit_mem = extract_post (CFG.Node.id exit_node) inv_map in
-    match exit_mem with
-    | Some exit_mem ->
-        let exit_mem = exit_mem |> Dom.Mem.forget_locs locals |> Dom.Mem.unset_oenv in
-        let payload = (exit_mem, cond_set) in
-        Payload.update_summary payload summary
-    | _ ->
-        summary
+    let exit_mem =
+      extract_post (CFG.Node.id exit_node) inv_map
+      |> Option.value ~default:Bottom |> Dom.Mem.forget_locs locals |> Dom.Mem.unset_oenv
+    in
+    let payload = (exit_mem, cond_set) in
+    Payload.update_summary payload summary
   in
   NodePrinter.finish_session underlying_exit_node ;
   if Config.hoisting_report_only_expensive then