[inferbo] Fix division by constant

Reviewed By: jvillard

Differential Revision: D6703065

fbshipit-source-id: 00e5f67

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. *)

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;
+}