making get_reachable_hpreds understand inductive predicates

Reviewed By: jvillard

Differential Revision: D3671401

fbshipit-source-id: 29e0f7e

infer/src/IR/Cfg.re

@@ -920,6 +920,22 @@ let remove_abducted_retvars p =>
               let exps' = collect_exps exps rhs;
               (reach', exps')
             }
+          | Sil.Hlseg _ _ exp1 exp2 exp_l as hpred => {
+              let reach' = Sil.HpredSet.add hpred reach;
+              let exps' =
+                IList.fold_left
+                  (fun exps_acc exp => Sil.ExpSet.add exp exps_acc) exps [exp1, exp2, ...exp_l];
+              (reach', exps')
+            }
+          | Sil.Hdllseg _ _ exp1 exp2 exp3 exp4 exp_l as hpred => {
+              let reach' = Sil.HpredSet.add hpred reach;
+              let exps' =
+                IList.fold_left
+                  (fun exps_acc exp => Sil.ExpSet.add exp exps_acc)
+                  exps
+                  [exp1, exp2, exp3, exp4, ...exp_l];
+              (reach', exps')
+            }
           | _ => (reach, exps);
         let (reach', exps') = IList.fold_left add_hpred_if_reachable (reach, exps) sigma;
         if (Sil.HpredSet.cardinal reach == Sil.HpredSet.cardinal reach') {

infer/tests/codetoanalyze/c/errors/lists/lists.c

@@ -7,6 +7,8 @@
  * of patent rights can be found in the PATENTS file in the same directory.
  */
 
+#include <stdlib.h>
+
 struct l2 {
   int b;
   struct l2* a;
@@ -25,3 +27,46 @@ int main() {
   int res = add2(0);
   return 5 / res;
 }
+
+typedef struct node { struct node* next; } T;
+
+void delete_one(T* x) { free(x); }
+
+void delete_all(T* x) {
+  T* temp;
+  while (x != NULL) {
+    temp = x;
+    x = x->next;
+    free(temp);
+  }
+}
+
+int call_delete() {
+  T* root = malloc(sizeof(T));
+  delete_one(root); // no memory leak should be reported here
+  return 0;
+}
+
+int call_delete_all1() {
+  T* root = malloc(sizeof(T));
+  delete_all(root); // no memory leak should be reported here
+  return 0;
+}
+
+int call_delete_all2() {
+  T* root = malloc(sizeof(T));
+  if (root != NULL) {
+    root->next = malloc(sizeof(T));
+  }
+  delete_all(root); // no memory leak should be reported here
+  return 0;
+}
+
+int call_all() {
+  int ret1 = call_delete();
+  int ret2 = call_delete_all1();
+  int ret3 = call_delete_all2();
+  // if any of the callees have precondition not met, we won't see div by zero
+  // here
+  return 1 / (ret1 + ret2 + ret3);
+}

infer/tests/endtoend/c/infer/ListsTest.java

@@ -36,7 +36,11 @@ public class ListsTest {
   @Test
   public void whenInferRunsOnDivideByZeroThenDivideByZeroIsFound()
       throws InterruptedException, IOException, InferException {
-    String[] procedures = {"main"};
+    String[] procedures =
+      { "main",
+        // TODO: fix me!
+        // "call_all"
+      };
     assertThat(
         "Results should contain divide by zero error",
         inferResults,