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, [,Assignment,,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,,Parameter `size`,,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,,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,,Parameter `idx`,,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,,Parameter `idx`,,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,,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,,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,,Parameter `*__il`,Array access: Offset: [-oo, +oo] Size: [0, +oo]]