NULL_DEREFERENCE not found when there are `&&` in loop conditions

[zyh1121]

I was playing with an OpenSSL function https://github.com/openssl/openssl/blob/5f96a95e2562f026557f625e50c052e77c7bc2e8/crypto/modes/cbc128.c#L55 and found this issue.

I came up with a few minimized examples to see why Infer missed the NULL_DEREFERENCE.

• Infer can capture them when there are no&& in the loop conditions in test1_1 and test2_1.
• However, if I changed the loop condition and added && (such as test1_2 or test1_3), infer missed the issues.
• I also tried and added || to loop condition. Infer can capture them correctly.

---

Please make sure your issue is not addressed in the FAQ.

Please include the following information:

• [x] The version of infer from infer --version.

$ infer --version
Infer version v1.1.0-119e20698
Copyright 2009 - present Facebook. All Rights Reserved.

• [x] Your operating system and version, for example "Debian 9", "MacOS High Sierra", whether you are using Docker, etc.

ubuntu 20.04 
5.8.0-50-generic #56~20.04.1-Ubuntu SMP 

• [x] Which command you ran, for example infer -- make.

infer run -- gcc -c 1.c

• [x] The full output in a paste, for instance a gist.

$ infer run -- gcc -c 1.c 
Capturing in make/cc mode...
Found 1 source file to analyze in /home/work/d2a/test/infer-out
1/1 [################################################################################] 100% 57.098ms

1.c:16: error: Null Dereference
  pointer `in` last assigned on line 14 could be null and is dereferenced at line 16, column 9.
  14.     const unsigned char *in = NULL;
  15.     while (len) {
  16.         * in;
              ^
  17.         len--;
  18.     }

1.c:41: error: Null Dereference
  pointer `in` last assigned on line 39 could be null and is dereferenced at line 41, column 9.
  39.     const unsigned char *in = NULL;
  40.     for (;len;) {
  41.         * in;
              ^
  42.         len--;
  43.     }


Found 2 issues
          Issue Type(ISSUED_TYPE_ID): #
  Null Dereference(NULL_DEREFERENCE): 2

• [x] If possible, a minimal example to reproduce your problem (for instance, some code where infer reports incorrectly, together with the way you run infer to reproduce the incorrect report).

#include <stdio.h>

void original(size_t len, const unsigned char *in, unsigned char *out) {
    size_t n = 0;
    in = NULL;
    while (len) {
        for (n = 0; n < 16 && n < len; ++n)
            out[n] = in[n];
        len -= 16;
    }
}

void test1_1(size_t len) {
    const unsigned char *in = NULL;
    while (len) {
        * in;
        len--;
    }
}

void test1_2(size_t len) {
    const unsigned char *in = NULL;
    while (len && len) {
        * in;
        len--;
    }
}

void test1_3(size_t len) {
    const unsigned char *in = NULL;
    while (len && len < 16) {
        * in;
        len--;
    }
}


void test2_1(size_t len) {
    const unsigned char *in = NULL;
    for (;len;) {
        * in;
        len--;
    }
}

void test2_2(size_t len) {
    const unsigned char *in = NULL;
    for (;len && len;) {
        * in;
        len--;
    }
}

void test2_3(size_t len) {
    const unsigned char *in = NULL;
    for (;len && len < 16;) {
        * in;
        len--;
    }
}

[jvillard]

Infer does find all the null dereference here but some of them are filtered out. You can see them with -F.

As an aside, the new pulse analysis (--pulse) also finds all the issues but doesn't report them straight away as they are only triggered on certain values of len (namely len ≠ 0). Pulse would report these bugs once these functions get called.