diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index a9fc921af..ee0660e72 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -464,6 +464,17 @@ let check_already_dereferenced tenv pname cond prop = | Exp.BinOp ((Binop.Eq | Binop.Ne), Exp.Var id, Exp.Const Const.Cint i) when IntLit.iszero i -> Some id + (* These two patterns appear frequently in Prune nodes *) + | Exp.BinOp + ( (Binop.Eq | Binop.Ne) + , Exp.BinOp (Binop.Eq, Exp.Var id, Exp.Const Const.Cint i) + , Exp.Const Const.Cint j ) + | Exp.BinOp + ( (Binop.Eq | Binop.Ne) + , Exp.BinOp (Binop.Eq, Exp.Const Const.Cint i, Exp.Var id) + , Exp.Const Const.Cint j ) + when IntLit.iszero i && IntLit.iszero j + -> Some id | _ -> None in diff --git a/infer/tests/codetoanalyze/c/errors/issues.exp b/infer/tests/codetoanalyze/c/errors/issues.exp index a0c7b3c49..85128b0bb 100644 --- a/infer/tests/codetoanalyze/c/errors/issues.exp +++ b/infer/tests/codetoanalyze/c/errors/issues.exp @@ -89,6 +89,7 @@ codetoanalyze/c/errors/null_dereference/short.c, g_error, 2, NULL_DEREFERENCE codetoanalyze/c/errors/null_dereference/short.c, g_error, 2, NULL_TEST_AFTER_DEREFERENCE codetoanalyze/c/errors/null_dereference/short.c, l_error, 2, NULL_DEREFERENCE codetoanalyze/c/errors/null_dereference/short.c, m, 2, NULL_TEST_AFTER_DEREFERENCE +codetoanalyze/c/errors/null_test_after_deref/basic.c, null_test_deref_basic_bad, 2, NULL_TEST_AFTER_DEREFERENCE codetoanalyze/c/errors/resource_leaks/leak.c, fileNotClosed, 5, RESOURCE_LEAK codetoanalyze/c/errors/resource_leaks/leak.c, socketNotClosed, 5, RESOURCE_LEAK codetoanalyze/c/errors/sizeof/sizeof_706.c, sentinel_bad, 0, DIVIDE_BY_ZERO diff --git a/infer/tests/codetoanalyze/c/errors/null_test_after_deref/basic.c b/infer/tests/codetoanalyze/c/errors/null_test_after_deref/basic.c new file mode 100644 index 000000000..21e5d5ad2 --- /dev/null +++ b/infer/tests/codetoanalyze/c/errors/null_test_after_deref/basic.c @@ -0,0 +1,23 @@ +/* + * 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. + */ +int null_test_deref_basic_bad(int* p) { + int ret = *p; + if (p == 0) + return -1; + return ret; +} + +int null_test_deref_basic_ok() { + int x = 0; + int* p = &x; + int ret = *p; + if (p == 0) + return -1; + return ret; +}