diff --git a/infer/src/IR/Cfg.re b/infer/src/IR/Cfg.re index ded15ea4a..7bf5fbc7f 100644 --- a/infer/src/IR/Cfg.re +++ b/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') { diff --git a/infer/tests/codetoanalyze/c/errors/lists/lists.c b/infer/tests/codetoanalyze/c/errors/lists/lists.c index e05fd485b..19ba2622a 100644 --- a/infer/tests/codetoanalyze/c/errors/lists/lists.c +++ b/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 + 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); +} diff --git a/infer/tests/endtoend/c/infer/ListsTest.java b/infer/tests/endtoend/c/infer/ListsTest.java index df525b151..e6054cca5 100644 --- a/infer/tests/endtoend/c/infer/ListsTest.java +++ b/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,