From 2da04b835d9638aa977389006537a295aa38dfcd Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Fri, 1 May 2020 03:57:58 -0700 Subject: [PATCH] [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 | 1 + infer/tests/codetoanalyze/c/pulse/issues.exp | 1 - infer/tests/codetoanalyze/c/pulse/nullptr.c | 2 +- 3 files changed, 2 insertions(+), 2 deletions(-) diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index d00b0b19b..a11684e96 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/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] diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp b/infer/tests/codetoanalyze/c/pulse/issues.exp index 5eef917a5..50b6c54ac 100644 --- a/infer/tests/codetoanalyze/c/pulse/issues.exp +++ b/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] diff --git a/infer/tests/codetoanalyze/c/pulse/nullptr.c b/infer/tests/codetoanalyze/c/pulse/nullptr.c index 5ec9011f9..88fd03ae1 100644 --- a/infer/tests/codetoanalyze/c/pulse/nullptr.c +++ b/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); }