False positives in Pulse when analyzing CUrl

[3393304070]

I intended to use infer pulse to analyze this bug: https://curl.se/mail/lib-2023-05/0013.html which strangely ended up not being detected, as it seems to be a simple UAF case. To manually debug I added the three lines below to the start of "ssh_check_fingerprint" (the vulnerable function in CVE):

int *ptr = malloc(sizeof(int*));
free(ptr);
*ptr = 1;

And pulse failed to recognize this bug too. However, if the three lines were to be inserted into the main function, or into "Curl_timediff()" and other functions explicitly called within the caller functions of which are mentioned in the report. Note that even if the three lines were inserted at "lib/conncache.c:455" (right before the first bug caught), pulse still wouldn't be able to catch the UAF.

According to various output of infer debug ssh_check_fingerprint is indeed not skipped by pulse. However the log file suggests that some nodes are unreachable.

In my experience it seems that the same issue of False Negatives also appear when detecting Memory Leak or Null Pointer Dereference in C.

Steps to reproduce:

git clone https://github.com/curl/curl.git
cd curl
git checkout 3467e89bb97e6c87c7 -f 
wget https://github.com/libssh2/libssh2/releases/download/libssh2-1.11.0/libssh2-1.11.0.tar.gz
tar -xvf libssh2-1.11.0.tar.gz
cd libssh2-1.11.0
./buildconf
./configure
make
sudo make install
cd ..
./buildconf
./configure --disable-shared --enable-static --without-ssl --with-libssh2=/usr/local/lib/
infer run --pulse-only --enable-issue-type USE_AFTER_FREE_LATENT -- make

• Infer version v1.2.0
• Debian 6.1.27-1kali1
• infer run --pulse-only --enable-issue-type USE_AFTER_FREE_LATENT -- make

[grandnew]

@3393304070 Hi, do you have any other examples of False Negatives when detecting Memory Leaks or Null Pointer Dereference?