Array size in struct or global scope not captured?

[zyh1121]

It seems the array size in the struct or global array is not captured so that the buffer overflow is not detected.

I prepared three minimized examples to show this (please refer to the test case below).

• In t1(), the size of structCharVoid.charFirst in memcpy(structCharVoid.charFirst, ... is defined by typedef struct _charVoid. Infer didn't report it.
• In t2(), the size of global_aaa in memcpy(global_aaa, ... is defined by char global_aaa[16];. Infer didn't report it.
• However, in t3(), if I define a local array char local_aaa[16];, infer could detect the buffer overrun in memcpy(local_aaa, ...

Maybe related to #993 and #948 (global)

---

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

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

run --bufferoverrun --pulse  --enable-issue-type ARRAY_OUT_OF_BOUNDS_L1 \
 --enable-issue-type ARRAY_OUT_OF_BOUNDS_L2  --enable-issue-type ARRAY_OUT_OF_BOUNDS_L3 \
 --enable-issue-type BUFFER_OVERRUN_L4  --enable-issue-type BUFFER_OVERRUN_L5 \
 --enable-issue-type BUFFER_OVERRUN_U5  --enable-issue-type INTEGER_OVERFLOW_L5 \
 --enable-issue-type INTEGER_OVERFLOW_U5 \
 -- gcc -c  test1.c 

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

Found 1 source file to analyze in /home/work/p2im/samples/CWE121/infer-out
1/1 [################################################################################] 100% 44.198ms

test1.c:26: error: Buffer Overrun L1
  Offset added: 24 Size: 16.
  24.     char local_aaa[16];
  25.     charVoid structCharVoid;
  26.     memcpy(local_aaa, SRC_STR, sizeof(structCharVoid));
          ^
  27. }


Found 1 issue
            Issue Type(ISSUED_TYPE_ID): #
  Buffer Overrun L1(BUFFER_OVERRUN_L1): 1

• [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>

#define SRC_STR "0123456789abcdef0123456789abcde"

typedef struct _charVoid
{
    char charFirst[16];
    void * voidSecond;
} charVoid;

char global_aaa[16];

void t1() {
    charVoid structCharVoid;
    memcpy(structCharVoid.charFirst, SRC_STR, sizeof(structCharVoid));
}

void t2() {
    charVoid structCharVoid;
    memcpy(global_aaa, SRC_STR, sizeof(structCharVoid));
}

void t3() {
    char local_aaa[16];
    charVoid structCharVoid;
    memcpy(local_aaa, SRC_STR, sizeof(structCharVoid));
}

[markdascher]

This seems to also result in false positives, since Infer sometimes guesses at the size each time you memcpy into it:

char foo[] = "foo";
char foobar[] = "foobar";

void t4() {
    memcpy(global_aaa, foo, sizeof foo);
    memcpy(global_aaa, foobar, sizeof foobar);
}

results in this error on the second memcpy:

main.c:33: error: Buffer Overrun L1
  Offset added: 7 Size: 4.