A false report in Infer 1.2.0

[Zustin]

Please make sure your issue is not addressed in the FAQ. I used infer to detect the following program. It is obvious that the program has a double free issue, but Infer reports a false warnign "use after free". See the log below.

double_free.c

#include <stdlib.h>

void double_free_example() {
    int *ptr = (int *)malloc(sizeof(int));
    if (ptr == NULL) {
        return;
    }
    free(ptr);
    free(ptr); // This is a double-free error
}

int main() {
    double_free_example();
    return 0;
}

Log

Capturing in make/cc mode...
Found 1 source file to analyze in /Users/rainyd4y/code/infer-out
3/3 [################################################################################] 100% 293ms

double_free.c:9: error: Use After Free
  accessing `ptr` that was invalidated by call to `free()` on line 8.
   7.     }
   8.     free(ptr);
   9.     free(ptr); // This is a double-free error
          ^
  10. }
  11.
Found 1 issue
      Issue Type(ISSUED_TYPE_ID): #
  Use After Free(USE_AFTER_FREE): 1

I used Infer 1.2.0 and MacOS version.