From 7b8dc59386529801f9a7fb67ead94053dbf53b42 Mon Sep 17 00:00:00 2001
From: Mehdi Bouaziz <mbouaziz@fb.com>
Date: Thu, 4 May 2017 03:04:08 -0700
Subject: [PATCH] [inferbo] Always use strong update

Summary:
For now we just want to find bugs, let's do something smarter later (smash heap variables only when needed).

Depends on D4962107

Reviewed By: jvillard

Differential Revision: D4962121

fbshipit-source-id: 1b777a6
---
 infer/src/bufferoverrun/bufferOverrunDomain.ml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml
index 6c9cf7a27..c3575fd7f 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomain.ml
+++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml
@@ -17,6 +17,8 @@ module F = Format
 module L = Logging
 module MF = MarkupFormatter
 
+let always_strong_update = true (* unsound but ok for bug catching *)
+
 module Condition =
 struct
   type t =
@@ -662,6 +664,7 @@ struct
 
   let can_strong_update : PowLoc.t -> bool
     = fun ploc ->
+      if always_strong_update then true else
       if Int.equal (PowLoc.cardinal ploc) 1 then Loc.is_var (PowLoc.choose ploc) else false
 
   let update_mem : PowLoc.t -> Val.t -> t -> t