ITADN

`sem.malloc.fail` makes memory leak analysis less precise

#2093Opensim642 创建于 15 天前
sv-compprecision
S
sim642commented
While reviewing https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1686, I did runs with `sem.malloc.fail` enabled and found differences in memory leak analysis. For example, the result for sv-benchmarks/c/ldv-memsafety/memleaks_test1-3.i changes. In particular, it seems that calling `free` on a pointer, which can be known or `NULL` is less precise than just with the known pointer in the memLeak analysis. However, that shouldn't be the case: `free(NULL)` is fine and a no-op.
0 条评论