diff --git a/Makefile b/Makefile index e4d5c26d49..f3ce8ec014 100644 --- a/Makefile +++ b/Makefile @@ -56,7 +56,8 @@ DIRECT_TESTS += \ c_bufferoverrun \ c_performance \ c_pulse \ - c_pulse-join \ + c_pulse-over-only \ + c_pulse-over-under \ c_purity \ c_starvation \ c_topl \ diff --git a/infer/tests/codetoanalyze/c/pulse-join/issues.exp b/infer/tests/codetoanalyze/c/pulse-join/issues.exp deleted file mode 100644 index f0a7e78e25..0000000000 --- a/infer/tests/codetoanalyze/c/pulse-join/issues.exp +++ /dev/null @@ -1,5 +0,0 @@ -codetoanalyze/c/pulse-join/attributes.c, init_one_branch_only_bad, 5, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `x` declared here,read to uninitialized value occurs here] -codetoanalyze/c/pulse-join/attributes.c, FNsuppressed_invalid_one_branch_only_bad, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** SUPPRESSED ***,source of the null value part of the trace starts here,assigned,is assigned to the null pointer,null pointer dereference part of the trace starts here,invalid access occurs here] -codetoanalyze/c/pulse-join/formula.c, FP_same_facts_different_branches_ok, 19, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here] -codetoanalyze/c/pulse-join/formula.c, FP_same_facts_different_branches_ok, 23, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here] -codetoanalyze/c/pulse-join/join.c, join_valid_invalid_pointers, 1, NULLPTR_DEREFERENCE_LATENT, no_bucket, ERROR, [*** SUPPRESSED ***,source of the null value part of the trace starts here,is assigned to the null pointer,null pointer dereference part of the trace starts here,parameter `p` of join_valid_invalid_pointers,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/c/pulse-join/Makefile b/infer/tests/codetoanalyze/c/pulse-over-only/Makefile similarity index 89% rename from infer/tests/codetoanalyze/c/pulse-join/Makefile rename to infer/tests/codetoanalyze/c/pulse-over-only/Makefile index cfc7f76dcf..f347a29800 100644 --- a/infer/tests/codetoanalyze/c/pulse-join/Makefile +++ b/infer/tests/codetoanalyze/c/pulse-over-only/Makefile @@ -5,6 +5,8 @@ TESTS_DIR = ../../.. +# Tests for the over-approximating pulse domain on its own + CLANG_OPTIONS = -c INFER_OPTIONS = \ --pulse-only --debug-exceptions --project-root $(TESTS_DIR) \ diff --git a/infer/tests/codetoanalyze/c/pulse-join/attributes.c b/infer/tests/codetoanalyze/c/pulse-over-only/attributes.c similarity index 100% rename from infer/tests/codetoanalyze/c/pulse-join/attributes.c rename to infer/tests/codetoanalyze/c/pulse-over-only/attributes.c diff --git a/infer/tests/codetoanalyze/c/pulse-join/formula.c b/infer/tests/codetoanalyze/c/pulse-over-only/formula.c similarity index 100% rename from infer/tests/codetoanalyze/c/pulse-join/formula.c rename to infer/tests/codetoanalyze/c/pulse-over-only/formula.c diff --git a/infer/tests/codetoanalyze/c/pulse-over-only/issues.exp b/infer/tests/codetoanalyze/c/pulse-over-only/issues.exp new file mode 100644 index 0000000000..65afd022ea --- /dev/null +++ b/infer/tests/codetoanalyze/c/pulse-over-only/issues.exp @@ -0,0 +1,5 @@ +codetoanalyze/c/pulse-over-only/attributes.c, init_one_branch_only_bad, 5, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `x` declared here,read to uninitialized value occurs here] +codetoanalyze/c/pulse-over-only/attributes.c, FNsuppressed_invalid_one_branch_only_bad, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** SUPPRESSED ***,source of the null value part of the trace starts here,assigned,is assigned to the null pointer,null pointer dereference part of the trace starts here,invalid access occurs here] +codetoanalyze/c/pulse-over-only/formula.c, FP_same_facts_different_branches_ok, 19, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here] +codetoanalyze/c/pulse-over-only/formula.c, FP_same_facts_different_branches_ok, 23, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here] +codetoanalyze/c/pulse-over-only/join.c, join_valid_invalid_pointers, 1, NULLPTR_DEREFERENCE_LATENT, no_bucket, ERROR, [*** SUPPRESSED ***,source of the null value part of the trace starts here,is assigned to the null pointer,null pointer dereference part of the trace starts here,parameter `p` of join_valid_invalid_pointers,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/c/pulse-join/join.c b/infer/tests/codetoanalyze/c/pulse-over-only/join.c similarity index 100% rename from infer/tests/codetoanalyze/c/pulse-join/join.c rename to infer/tests/codetoanalyze/c/pulse-over-only/join.c diff --git a/infer/tests/codetoanalyze/c/pulse-over-under/Makefile b/infer/tests/codetoanalyze/c/pulse-over-under/Makefile new file mode 100644 index 0000000000..a8d902dca1 --- /dev/null +++ b/infer/tests/codetoanalyze/c/pulse-over-under/Makefile @@ -0,0 +1,20 @@ +# Copyright (c) Facebook, Inc. and its affiliates. +# +# This source code is licensed under the MIT license found in the +# LICENSE file in the root directory of this source tree. + +TESTS_DIR = ../../.. + +# Tests for the over-approximating pulse domain mixed with the disjunctive domain + +CLANG_OPTIONS = -c +INFER_OPTIONS = \ + --pulse-only --debug-exceptions --project-root $(TESTS_DIR) \ + --pulse-report-issues-for-tests --no-pulse-force-continue \ + --pulse-max-disjuncts 1 --pulse-over-approximate-reasoning \ + +INFERPRINT_OPTIONS = --issues-tests + +SOURCES = $(wildcard *.c */*.c) + +include $(TESTS_DIR)/clang.make diff --git a/infer/tests/codetoanalyze/c/pulse-over-under/issues.exp b/infer/tests/codetoanalyze/c/pulse-over-under/issues.exp new file mode 100644 index 0000000000..3e7bc56dbc --- /dev/null +++ b/infer/tests/codetoanalyze/c/pulse-over-under/issues.exp @@ -0,0 +1,2 @@ +codetoanalyze/c/pulse-over-under/join.c, FP_join_strong_update_ok, 10, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [read to uninitialized value occurs here] +codetoanalyze/c/pulse-over-under/join.c, FP_join_strong_update_ok, 13, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/c/pulse-over-under/join.c b/infer/tests/codetoanalyze/c/pulse-over-under/join.c new file mode 100644 index 0000000000..7a42072c7f --- /dev/null +++ b/infer/tests/codetoanalyze/c/pulse-over-under/join.c @@ -0,0 +1,27 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +// best run with --pulse-max-disjuncts 1 --pulse-over-approximate-reasoning + +#include + +void FP_join_strong_update_ok() { + int x; + int z = 0; + if (random()) { + x = z; + } else { + x = z; + } + // could be an uninit FP if x's assignments disappear + int y = x; + if (y != 0) { + // could be a null deref FP if x is not strongly updated after branching + int* p = NULL; + *p = 42; + } +}