[pulse][join] tests for over+under combination

Summary:
Rename the test directory "pulse-join/" to "pulse-over-only/" and add a
new test directory for the combination of under + over domains, running
with ` --pulse-max-disjuncts 1` (whereas "pulse-over-only" tests run
with ` --pulse-max-disjuncts 0`, which disables the disjunctive domain).

Reviewed By: ngorogiannis

Differential Revision:
D66972974

Privacy Context Container: L1208441

fbshipit-source-id: 8b15931f443aaf2a01be188647bd8c6cbbbc3488

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 \

infer/tests/codetoanalyze/c/pulse-join/Makefile → 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) \

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]

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

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]

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 <stdlib.h>
+
+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;
+  }
+}