[biabduction][test] Repro of issue 680

Reviewed By: jvillard

Differential Revision: D5347155

fbshipit-source-id: 99b9cd8

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

@@ -72,6 +72,9 @@ codetoanalyze/c/errors/null_dereference/getc.c, crash_ungetc, 5, NULL_DEREFERENC
 codetoanalyze/c/errors/null_dereference/getc.c, crash_ungetc, 5, RETURN_VALUE_IGNORED
 codetoanalyze/c/errors/null_dereference/getc.c, crash_vfprintf, 5, NULL_DEREFERENCE
 codetoanalyze/c/errors/null_dereference/getc.c, nocrash_ungetc, 5, RETURN_VALUE_IGNORED
+codetoanalyze/c/errors/null_dereference/issue_680.c, null_ptr_deref2_bad, 0, NULL_DEREFERENCE
+codetoanalyze/c/errors/null_dereference/issue_680.c, null_ptr_deref_bad, 0, NULL_DEREFERENCE
+codetoanalyze/c/errors/null_dereference/issue_680.c, null_ptr_deref_bad_FN, 0, PRECONDITION_NOT_MET
 codetoanalyze/c/errors/null_dereference/malloc_no_null_check.c, test_malloc, 2, NULL_DEREFERENCE
 codetoanalyze/c/errors/null_dereference/memcpy-test.c, testError1, 3, NULL_DEREFERENCE
 codetoanalyze/c/errors/null_dereference/memcpy-test.c, testError2, 5, NULL_DEREFERENCE

infer/tests/codetoanalyze/c/errors/null_dereference/issue_680.c

@@ -0,0 +1,37 @@
+/*
+ * 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.
+ */
+#include <stdlib.h>
+
+struct list {
+  struct list* next;
+};
+
+void go_to_next(struct list* head) {
+  if (head->next != NULL) {
+    head = head->next;
+  }
+}
+
+void null_ptr_deref_bad() { go_to_next(NULL); }
+
+void go_to_end_of_list(struct list* head) {
+  while (head->next != NULL) {
+    head = head->next;
+  }
+}
+
+void null_ptr_deref_bad_FN() { go_to_end_of_list(NULL); }
+
+void check_next(struct list* head) {
+  while (head->next != NULL) {
+    whatever();
+  }
+}
+
+void null_ptr_deref2_bad() { check_next(NULL); }