From 09a5671ef4c2313cf30ee14fe67ec94819b4ebb3 Mon Sep 17 00:00:00 2001
From: Sungkeun Cho <scho@fb.com>
Date: Tue, 22 Jan 2019 00:51:41 -0800
Subject: [PATCH] [inferbo] Add a test for conditional inequality

Reviewed By: mbouaziz

Differential Revision: D13729600

fbshipit-source-id: d460093e1
---
 .../bufferoverrun/conditional_proof_obligation.cpp   | 12 ++++++++++++
 .../tests/codetoanalyze/cpp/bufferoverrun/issues.exp |  2 ++
 2 files changed, 14 insertions(+)

diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp
index 354dd5a2c..07ab1c7ca 100644
--- a/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp
+++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp
@@ -117,3 +117,15 @@ void call_conditional_buffer_access3_Bad() {
   a[0] = E_SIZETWO;
   conditional_buffer_access3(a, 1);
 }
+
+void conditional_inequality(int idx) {
+  int a[5];
+  if (idx == 5) {
+  } else {
+    a[idx] = 0;
+  }
+}
+
+void call_conditional_inequality_Good_FP() { conditional_inequality(5); }
+
+void call_conditional_inequality_Bad() { conditional_inequality(6); }
diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp
index e747b2fde..57f34b2be 100644
--- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp
+++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp
@@ -35,6 +35,8 @@ codetoanalyze/cpp/bufferoverrun/class.cpp, return_class_Bad, 2, BUFFER_OVERRUN_L
 codetoanalyze/cpp/bufferoverrun/class.cpp, use_global_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 32 Size: 30]
 codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access3_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Parameter `size`,<Length trace>,Parameter `*ptr`,Array access: Offset: -1 Size: 1 by call to `conditional_buffer_access3` ]
 codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Parameter `*ptr`,Assignment,Assignment,Array access: Offset: 2 Size: 1 by call to `conditional_buffer_access` ]
+codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_inequality_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `idx`,<Length trace>,Array declaration,Array access: Offset: 6 Size: 5 by call to `conditional_inequality` ]
+codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_inequality_Good_FP, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `idx`,<Length trace>,Array declaration,Array access: Offset: 5 Size: 5 by call to `conditional_inequality` ]
 codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus2_2_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,<LHS trace>,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus2` ]
 codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus_2_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,<LHS trace>,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus` ]
 codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 1, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: __infer_skip_function,Call,<Length trace>,Parameter `*__il`,Array access: Offset: [-oo, +oo] Size: [0, +oo]]