diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index fa5f324a1..b7e60cadc 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -1260,6 +1260,14 @@ module Normalize = struct -> if Exp.equal idx1 idx2 then normalize_eq (e1', e2') else if Exp.equal e1' e2' then normalize_eq (idx1, idx2) else eq + | BinOp ((PlusA | PlusPI | MinusA | MinusPI), e1, e2), e1' when Exp.equal e1 e1' + -> (e2, Exp.int IntLit.zero) + | BinOp ((PlusA | PlusPI), e2, e1), e1' when Exp.equal e1 e1' + -> (e2, Exp.int IntLit.zero) + | e1', BinOp ((PlusA | PlusPI | MinusA | MinusPI), e1, e2) when Exp.equal e1 e1' + -> (e2, Exp.int IntLit.zero) + | e1', BinOp ((PlusA | PlusPI), e2, e1) when Exp.equal e1 e1' + -> (e2, Exp.int IntLit.zero) | _ -> eq in diff --git a/infer/tests/codetoanalyze/cpp/errors/issues.exp b/infer/tests/codetoanalyze/cpp/errors/issues.exp index 3c78eb05e..06879ffda 100644 --- a/infer/tests/codetoanalyze/cpp/errors/issues.exp +++ b/infer/tests/codetoanalyze/cpp/errors/issues.exp @@ -49,6 +49,10 @@ codetoanalyze/cpp/errors/npe/boxed_ptr.cpp, boxed_ptr::smart_ptr_null_method_der codetoanalyze/cpp/errors/npe/boxed_ptr.cpp, boxed_ptr::smart_ptr_ok_field_deref, 4, UNINITIALIZED_VALUE, [start of procedure boxed_ptr::smart_ptr_ok_field_deref(),start of procedure SmartPtr,return from a call to boxed_ptr::SmartPtr_SmartPtr,start of procedure X,return from a call to boxed_ptr::X_X,start of procedure get,return from a call to boxed_ptr::SmartPtr_get] codetoanalyze/cpp/errors/npe/boxed_ptr.cpp, boxed_ptr::smart_ptr_result_method_null_deref, 4, NULL_DEREFERENCE, [start of procedure boxed_ptr::smart_ptr_result_method_null_deref(),start of procedure SmartPtr,return from a call to boxed_ptr::SmartPtr_SmartPtr,start of procedure X,return from a call to boxed_ptr::X_X,start of procedure get,return from a call to boxed_ptr::SmartPtr_get,start of procedure getNull,return from a call to boxed_ptr::X_getNull] codetoanalyze/cpp/errors/npe/boxed_ptr.cpp, boxed_ptr::smart_ptr_result_method_ok_deref, 4, UNINITIALIZED_VALUE, [start of procedure boxed_ptr::smart_ptr_result_method_ok_deref(),start of procedure SmartPtr,return from a call to boxed_ptr::SmartPtr_SmartPtr,start of procedure X,return from a call to boxed_ptr::X_X,start of procedure get,return from a call to boxed_ptr::SmartPtr_get,start of procedure getPtr,return from a call to boxed_ptr::X_getPtr] +codetoanalyze/cpp/errors/npe/cancellation.cpp, cancellation_test::size_nonzero_deref2_bad, 4, NULL_DEREFERENCE, [start of procedure cancellation_test::size_nonzero_deref2_bad(),start of procedure cancellation_test::is_size_zero(),start of procedure begin,return from a call to cancellation_test::Test_begin,start of procedure end,return from a call to cancellation_test::Test_end,Condition is false,return from a call to cancellation_test::is_size_zero,Condition is false,Condition is true] +codetoanalyze/cpp/errors/npe/cancellation.cpp, cancellation_test::size_nonzero_deref_bad, 4, NULL_DEREFERENCE, [start of procedure cancellation_test::size_nonzero_deref_bad(),start of procedure cancellation_test::is_size_zero(),start of procedure begin,return from a call to cancellation_test::Test_begin,start of procedure end,return from a call to cancellation_test::Test_end,Condition is false,return from a call to cancellation_test::is_size_zero,Condition is false,Condition is true] +codetoanalyze/cpp/errors/npe/cancellation.cpp, cancellation_test::size_zero_deref2_bad, 4, NULL_DEREFERENCE, [start of procedure cancellation_test::size_zero_deref2_bad(),start of procedure cancellation_test::is_size_zero(),start of procedure begin,return from a call to cancellation_test::Test_begin,start of procedure end,return from a call to cancellation_test::Test_end,Condition is true,return from a call to cancellation_test::is_size_zero,Condition is true] +codetoanalyze/cpp/errors/npe/cancellation.cpp, cancellation_test::size_zero_deref_bad, 4, NULL_DEREFERENCE, [start of procedure cancellation_test::size_zero_deref_bad(),start of procedure cancellation_test::is_size_zero(),start of procedure begin,return from a call to cancellation_test::Test_begin,start of procedure end,return from a call to cancellation_test::Test_end,Condition is true,return from a call to cancellation_test::is_size_zero,Condition is true] codetoanalyze/cpp/errors/npe/npe_added_to_b1.cpp, npe_added_to_b1::causes_npe, 2, NULL_DEREFERENCE, [start of procedure npe_added_to_b1::causes_npe(),start of procedure npe_added_to_b1::deref_ref()] codetoanalyze/cpp/errors/npe/npe_added_to_b1.cpp, npe_added_to_b1::causes_npe_person, 2, NULL_DEREFERENCE, [start of procedure npe_added_to_b1::causes_npe_person(),start of procedure Person,return from a call to npe_added_to_b1::Person_Person,start of procedure npe_added_to_b1::deref_person()] codetoanalyze/cpp/errors/npe/null_returned_by_method.cpp, testNullDeref, 3, NULL_DEREFERENCE, [start of procedure testNullDeref(),Condition is true,start of procedure getNull,return from a call to XFactory_getNull] diff --git a/infer/tests/codetoanalyze/cpp/errors/npe/cancellation.cpp b/infer/tests/codetoanalyze/cpp/errors/npe/cancellation.cpp new file mode 100644 index 000000000..dabde519c --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/errors/npe/cancellation.cpp @@ -0,0 +1,77 @@ +/* + * Copyright (c) 2017 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ +namespace cancellation_test { + +struct Test { + int x, sz; + + int begin() const { return x; } + int end() const { return x + sz; } + int end2() const { return x - sz; } +}; + +bool is_size_zero(const Test& t) { return t.begin() == t.end(); } +bool is_size_zero2(const Test& t) { return t.begin() == t.end2(); } + +void size_zero_no_deref_ok() { + int* p = nullptr; + Test t{1, 0}; + if (!is_size_zero(t)) + *p = 42; +} + +void size_zero_deref_bad() { + int* p = nullptr; + Test t{1, 0}; + if (is_size_zero(t)) + *p = 42; +} + +void size_nonzero_no_deref2_ok() { + int* p = nullptr; + Test t{1, 1}; + if (is_size_zero(t)) + *p = 42; +} + +void size_nonzero_deref2_bad() { + int* p = nullptr; + Test t{1, 1}; + if (!is_size_zero(t)) + *p = 42; +} + +void size_zero_no_deref2_ok() { + int* p = nullptr; + Test t{1, 0}; + if (!is_size_zero(t)) + *p = 42; +} + +void size_zero_deref2_bad() { + int* p = nullptr; + Test t{1, 0}; + if (is_size_zero(t)) + *p = 42; +} + +void size_nonzero_no_deref_ok() { + int* p = nullptr; + Test t{1, 1}; + if (is_size_zero(t)) + *p = 42; +} + +void size_nonzero_deref_bad() { + int* p = nullptr; + Test t{1, 1}; + if (!is_size_zero(t)) + *p = 42; +} +} // namespace cancellation_test