[pulse] require ptr>0 in free()

Summary: Resolves a false positive.

Reviewed By: skcho

Differential Revision: D21332074

fbshipit-source-id: a0c962b91

infer/src/pulse/PulseModels.ml

@@ -78,6 +78,7 @@ module C = struct
     if PulseArithmetic.is_known_zero astate (fst deleted_access) then
       PulseOperations.ok_continue astate
     else
+      let astate = PulseArithmetic.and_positive (fst deleted_access) astate in
       let+ astate = PulseOperations.invalidate location Invalidation.CFree deleted_access astate in
       [ExecutionDomain.ContinueProgram astate]
 

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

@@ -1,6 +1,5 @@
 codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad, 0, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `create_p` here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
 codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad2, 4, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
 codetoanalyze/c/pulse/memory_leak.c, malloc_no_free_bad, 0, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
-codetoanalyze/c/pulse/nullptr.c, FP_interproc_free_ok, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,allocated by call to `malloc` (modelled),is the null pointer,use-after-lifetime part of the trace starts here,allocated by call to `malloc` (modelled),assigned,when calling `wrap_free` here,parameter `p` of wrap_free,invalid access occurs here]
 codetoanalyze/c/pulse/nullptr.c, malloc_no_check_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,allocated by call to `malloc` (modelled),is the null pointer,use-after-lifetime part of the trace starts here,allocated by call to `malloc` (modelled),assigned,invalid access occurs here]
 codetoanalyze/c/pulse/nullptr.c, nullptr_deref_young_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]

infer/tests/codetoanalyze/c/pulse/nullptr.c

@@ -73,7 +73,7 @@ void malloc_free_ok() {
 
 void wrap_free(void* p) { free(p); }
 
-void FP_interproc_free_ok() {
+void interproc_free_ok() {
   int* p = (int*)malloc(sizeof(int));
   wrap_free(p);
 }