False positive on Infer and small struct.

check_foo_eats_nonNULL.txt

$ cat main.c
#include <stdio.h>

#define __infer_assert(E) {  \
  int *s = NULL;             \
  if (!(E)) *s = 0xDEADBEEF; \
}

struct foo {
        char *p;
};

void check_foo (struct foo *f) {
#if 1
        __infer_assert(f && f->p == NULL);
#endif
}

int main() {
#if 0
        struct foo f = { NULL };
#else
        char c;
        struct foo f = { &c };
#endif
        check_foo(&f);
}
casper$ make verify
infer -- gcc -c main.c
Infer version v0.9.4-e757d92
Copyright 2009 - present Facebook. All Rights Reserved.
Starting analysis (Infer version v0.9.4-e757d92)

legend:
  "F" analyzing a file
  "." analyzing a procedure

F..
Analyzed 1 file

Found 1 issue

main.c:14: error: NULL_DEREFERENCE
  pointer s last assigned on line 14 could be null and is dereferenced at line 14, column 2
  12.   void check_foo (struct foo *f) {
  13.   #if 1
  14. >         __infer_assert(f && f->p == NULL);
  15.   #endif
  16.   }
  17.   

Summary of the reports

  NULL_DEREFERENCE: 1

$ infer -g -- gcc -c main.c
--snip--
make -k -j 4 -l 4.0

/home/kiwamu/src/infer/infer/bin/InferAnalyze -results_dir '/home/kiwamu/src/practice-infer/inited/infer-out' -cluster xcl1.cluster >cl1
F..
Analyzed 1 file

Found 4 issues

main.c:14: error: NULL_DEREFERENCE (backend/rearrange.ml:1322:57-64:)
  [B1] pointer s last assigned on line 14 could be null and is dereferenced at line 14, column 2
  12.   void check_foo (struct foo *f) {
  13.   #if 1
  14. >         __infer_assert(f && f->p == NULL);
  15.   #endif
  16.   }
  17.   

main.c:14: warning: ANALYSIS_STOPS (backend/rearrange.ml:1322:57-64:)
  exception: NULL_DEREFERENCE
  12.   void check_foo (struct foo *f) {
  13.   #if 1
  14. >         __infer_assert(f && f->p == NULL);
  15.   #endif
  16.   }
  17.   

main.c:25: warning: PRECONDITION_NOT_MET (backend/tabulation.ml:1208:60-67:)
  in call to check_foo() at line 25, column 2
  23.           struct foo f = { &c };
  24.   #endif
  25. >         check_foo(&f);
  26.   }
  27.   

main.c:25: warning: ANALYSIS_STOPS (backend/tabulation.ml:1208:60-67:)
  exception: PRECONDITION_NOT_MET
  23.           struct foo f = { &c };
  24.   #endif
  25. >         check_foo(&f);
  26.   }
  27.   

Summary of the reports

        ANALYSIS_STOPS: 2
      NULL_DEREFERENCE: 1
  PRECONDITION_NOT_MET: 1

check_foo_eats_NULL.txt

$ cat main.c
#include <stdio.h>

#define __infer_assert(E) {  \
  int *s = NULL;             \
  if (!(E)) *s = 0xDEADBEEF; \
}

struct foo {
        char *p;
};

void check_foo (struct foo *f) {
#if 1   
        __infer_assert(f && f->p == NULL);
#endif
}

int main() {
#if 1   
        struct foo f = { NULL };
#else   
        char c;
        struct foo f = { &c };
#endif  
        check_foo(&f);
}
casper$ make verify
infer -- gcc -c main.c
Infer version v0.9.4-e757d92
Copyright 2009 - present Facebook. All Rights Reserved.
Starting analysis (Infer version v0.9.4-e757d92)

legend:
  "F" analyzing a file
  "." analyzing a procedure

F..
Analyzed 1 file

Found 1 issue

main.c:14: error: NULL_DEREFERENCE
  pointer s last assigned on line 14 could be null and is dereferenced at line 14, column 2
  12.   void check_foo (struct foo *f) {
  13.   #if 1
  14. >         __infer_assert(f && f->p == NULL);
  15.   #endif
  16.   }
  17.

Summary of the reports

  NULL_DEREFERENCE: 1

$ infer -g -- gcc -c main.c
--snip--
make -k -j 4 -l 4.0

/home/kiwamu/src/infer/infer/bin/InferAnalyze -results_dir '/home/kiwamu/src/practice-infer/inited/infer-out' -cluster xcl1.cluster >cl1
F..
Analyzed 1 file

Found 2 issues

main.c:14: error: NULL_DEREFERENCE (backend/rearrange.ml:1322:57-64:)
  [B1] pointer s last assigned on line 14 could be null and is dereferenced at line 14, column 2
  12.   void check_foo (struct foo *f) {
  13.   #if 1
  14. >         __infer_assert(f && f->p == NULL);
  15.   #endif
  16.   }
  17.   

main.c:14: warning: ANALYSIS_STOPS (backend/rearrange.ml:1322:57-64:)
  exception: NULL_DEREFERENCE
  12.   void check_foo (struct foo *f) {
  13.   #if 1
  14. >         __infer_assert(f && f->p == NULL);
  15.   #endif
  16.   }
  17.   

Summary of the reports

  NULL_DEREFERENCE: 1
    ANALYSIS_STOPS: 1