ISL tests

Reviewed By: jvillard

Differential Revision: D24433559

fbshipit-source-id: 4d7a4c221

infer/tests/codetoanalyze/c/pulse/Makefile

@@ -6,7 +6,8 @@
 TESTS_DIR = ../../..
 
 CLANG_OPTIONS = -c
-INFER_OPTIONS = --pulse-only --debug-exceptions --project-root $(TESTS_DIR)
+INFER_OPTIONS = --pulse-only --debug-exceptions --project-root $(TESTS_DIR) \
+  --pulse-report-latent-issues
 
 INFERPRINT_OPTIONS = --issues-tests
 

infer/tests/codetoanalyze/c/pulse/interprocedural.c

@@ -0,0 +1,22 @@
+/*
+ * 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.
+ */
+#include <stdlib.h>
+
+void if_freed_invalid_latent(int x, int* y) {
+  if (x > 5) {
+    free(y);
+    *y = 1;
+  }
+}
+
+void FN_call_if_freed_invalid_latent(int x) {
+  if (x > 0) {
+    if_freed_invalid(x, NULL);
+  }
+}
+
+void FN_call_if_freed_invalid2_bad() { call_if_freed_invalid(7); }

infer/tests/codetoanalyze/c/pulse/issues.exp

@@ -1,3 +1,4 @@
+codetoanalyze/c/pulse/interprocedural.c, if_freed_invalid_latent, 3, USE_AFTER_FREE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `y` of if_freed_invalid_latent,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `y` of if_freed_invalid_latent,invalid access occurs here]
 codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `create_p` here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
 codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad2, 4, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
 codetoanalyze/c/pulse/memory_leak.c, malloc_no_free_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here]