[inferbo] Ignore float/double constant

Summary:
Current domain of Inferbo cannot handle float values. This diff evaluates float constants to the top
interval.

Reviewed By: ezgicicek

Differential Revision: D20116361

fbshipit-source-id: e6e398bbd

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -18,8 +18,6 @@ let eval_const : Typ.IntegerWidths.t -> Const.t -> Val.t =
  fun integer_type_widths -> function
   | Const.Cint intlit ->
       Val.of_big_int (IntLit.to_big_int intlit)
-  | Const.Cfloat f ->
-      f |> int_of_float |> Val.of_int
   | Const.Cstr s ->
       Val.of_literal_string integer_type_widths s
   | _ ->

infer/tests/codetoanalyze/c/bufferoverrun/arith.c

@@ -572,3 +572,19 @@ void ptr_band2_Bad(int x, int* q) {
   }
   a[10] = 0;
 }
+
+void do_not_prune_float_Good_FP() {
+  int a[5];
+  float f = 0.5;
+  if (f > 1.0 && f < 1.0) {
+    a[10] = 0;
+  }
+}
+
+void do_not_prune_float_Bad() {
+  int a[5];
+  float f = 0.5;
+  if (f > 0.0 && f < 1.0) {
+    a[10] = 0;
+  }
+}

infer/tests/codetoanalyze/c/bufferoverrun/cast.c

@@ -72,7 +72,7 @@ void cast_signed_to_unsigned2_Bad_FN() {
   }
 }
 
-void cast_float_to_int_Good() {
+void cast_float_to_int_Good_FP() {
   char arr[10];
   float x = 15.0;
   int32_t y = (int32_t)x;
@@ -81,7 +81,7 @@ void cast_float_to_int_Good() {
   }
 }
 
-void cast_float_to_int_Bad_FN() {
+void cast_float_to_int_Bad() {
   char arr[10];
   float x = 15000000000.0;
   int32_t y = (int32_t)x; // y is -2147483648.

infer/tests/codetoanalyze/c/bufferoverrun/issues.exp

@@ -12,6 +12,8 @@ codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLO
 codetoanalyze/c/bufferoverrun/arith.c, call_two_safety_conditions2_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,<LHS trace>,Call,Assignment,Assignment,<RHS trace>,Parameter `s`,Binary operation: ([0, +oo] + 15):unsigned32 by call to `two_safety_conditions2_Bad` ]
 codetoanalyze/c/bufferoverrun/arith.c, div_const2_FP, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Parameter `n`,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 1]
 codetoanalyze/c/bufferoverrun/arith.c, div_const_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 2 Size: 2]
+codetoanalyze/c/bufferoverrun/arith.c, do_not_prune_float_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
+codetoanalyze/c/bufferoverrun/arith.c, do_not_prune_float_Good_FP, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
 codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Assignment,Binary operation: (2000000000 + 2000000000):signed32]
 codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_Bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_l2_Bad, 7, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Assignment,Binary operation: ([0, 2000000000] + [0, 2000000000]):signed32]
@@ -81,8 +83,8 @@ codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 16
 codetoanalyze/c/bufferoverrun/calloc.c, calloc_bad1, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: -1 Size: 10]
 codetoanalyze/c/bufferoverrun/calloc.c, calloc_bad1, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/cast.c, cast2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 20 Size: 16]
-codetoanalyze/c/bufferoverrun/cast.c, cast_float_to_int_Bad_FN, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
-codetoanalyze/c/bufferoverrun/cast.c, cast_float_to_int_Good, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
+codetoanalyze/c/bufferoverrun/cast.c, cast_float_to_int_Bad, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, 9] Size: 10]
+codetoanalyze/c/bufferoverrun/cast.c, cast_float_to_int_Good_FP, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, 9] Size: 10]
 codetoanalyze/c/bufferoverrun/cast.c, cast_signed_to_unsigned2_Bad_FN, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/cast.c, cast_signed_to_unsigned_Bad, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/cast.c, cast_signed_to_unsigned_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: 4294967295 Size: 10]