From d71d759344200aab4f54d835d33a1772355834b4 Mon Sep 17 00:00:00 2001
From: Mehdi Bouaziz <mbouaziz@fb.com>
Date: Fri, 12 Jan 2018 06:04:07 -0800
Subject: [PATCH] [inferbo] Fix division by constant

Reviewed By: jvillard

Differential Revision: D6703065

fbshipit-source-id: 00e5f67
---
 infer/src/bufferoverrun/itv.ml                    | 2 +-
 infer/tests/codetoanalyze/c/bufferoverrun/arith.c | 7 +++++++
 2 files changed, 8 insertions(+), 1 deletion(-)

diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml
index 1b8c52311..b508d3e5d 100644
--- a/infer/src/bufferoverrun/itv.ml
+++ b/infer/src/bufferoverrun/itv.ml
@@ -157,7 +157,7 @@ module SymLinear = struct
 
   let mult_const : t -> int -> t = fun x n -> M.map (( * ) n) x
 
-  let div_const : t -> int -> t = fun x n -> M.map (( / ) n) x
+  let div_const : t -> int -> t = fun x n -> M.map (fun c -> c / n) x
 
   (* Returns a symbol when the map contains only one symbol s with a
      given coefficient. *)
diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c
index 19717db8a..20fa32822 100644
--- a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c
+++ b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c
@@ -73,3 +73,10 @@ void modulo_call_Bad_FN(unsigned int len, int i) {
   char arr[len];
   arr[modulo_signed(i, len)] = 123;
 }
+
+int division_of_zero_Good(int x) {
+  int i = 4 * x;
+  i /= 2;
+  i /= 2;
+  return i;
+}