facebook / facebook/infer

[C] InferBO false positive

Open
#1,646 0 comments 1 reaction 0 assignees View on GitHub
c false-positive
Dominant language
OCaml
Stars
15.7k
Forks
2.1k
Avg merge
19h 36m
Merged PRs (30d)
13

Description

Please make sure your issue is not addressed in the [FAQ](https://fbinfer.com/docs/support#troubleshooting).

Please include the following information:
- [x] The version of infer from `infer --version`.
v1.1.0
- [x] Your operating system and version, for example "Debian 9", "MacOS High Sierra", whether you are using Docker, etc.
Ubuntu 22.04, bare metal
- [x] Which command you ran, for example `infer -- make`.
`infer -- gcc test.c`
- [x] The full output in a paste, for instance a [gist](https://gist.github.com/).
https://gist.github.com/mianowill/4e2ec778d8f4e28af6727170cb2e54cb
- [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).

I initially ran into this issue running `infer run --compilation-database build/compile_commands.json` on a CMake project, and created a small demo file to verify. There's an array which contains a pointer to an array we want to iterate through, and a `size_t` of the size of the array, such as

```c
lookup_array = {
[FOO] = {
.array_size = sizeof(bar) / sizeof(bar[0]),
.array_ptr = &bar[0]
},
...
}
```

Given two inputs `x` and `y`, the code checks to see if `y` is present in the array at `lookup_array[x].array_ptr`.
```c
bool function(data_t x, data_t y) {
for (size_t i = 0; i < lookup_array[x].array_size; i++) {
if (lookup_array[x].array_ptr[i] == y) {
return true;
}
}

return false;
}
```

The for-loop will iterate exactly once for each element in the array, given `.array_size = sizeof(bar) / sizeof(bar[0])`, however Infer believes the loop to iterate as many times as the number of elements of the largest array; that is, if we have an array of size 2 and an array of size 4, it will incorrectly deduce that the array of size 2 will be accessed with offset [0,3] and overrun at size 2.

Contributor guide

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.