facebook / facebook/infer

Infer issue with enum type

未关闭
#1,094 2 条评论 0 个 reaction 已指派 0 人 在 GitHub 查看
主要语言
OCaml
星标
15.7k
派生
2.1k
平均合并
19 小时 36 分钟
30 天内合并 PR
13

描述

Infer version: 0.16.0
OS: Ubuntu 18.04
Command:
```
infer --debug --print-logs --bufferoverrun --compute-analytics --biabduction --quandary -- make
```

Here is a minimal example where the array-out-of-bounds bug at `arr[10] = 1` is not discovered by Infer:

```c
char *kwsincr()
{
register int depth;
enum { L, R } dirs[12];


char arr[10];
if (depth < 10) {
/* POTENTIAL FLAW */
arr[10] = 1;
}

return 0;
}
```

Removing the line `enum { L, R } dirs[12]` causes Infer to find the error. Somehow, this enum line is interfering with the analysis.

I have run this minimal example with debug printing, and it turns out that the enum is indeed causing troubles, the log file contains the error:
```
[8199][ debug] Aborting translation of method 'kwsincr' in file 'minimal.c'
[8199][ debug] Unimplemented feature:
[8199][ debug] In DeclStmt found an unknown declaration type <"EnumDecl":({"pointer":19,"source_range":({"file":"/data/work/STAMP/bug_triage/tools/INFER-REGRESSION-TEST-BUFFER1-000009/minimal.c","line":8,"column":3},{"file":"/data/work/STAMP/bug_triage/tools/INFER-REGRESSION-TEST-BUFFER1-000009/minimal.c","line":8,"column":15})},{"name":"","qual_name":["anonymous_enum_minimal.c:8:3","kwsincr"]},20,[<"EnumConstantDecl":({"pointer":21,"source_range":({"file":"/data/work/STAMP/bug_triage/tools/INFER-REGRESSION-TEST-BUFFER1-000009/minimal.c","line":8,"column":10},{"file":"/data/work/STAMP/bug_triage/tools/INFER-REGRESSION-TEST-BUFFER1-000009/minimal.c","line":8,"column":10})},{"name":"L","qual_name":["L","anonymous_enum_minimal.c:8:3","kwsincr"]},{"type_ptr":10},{})>,<"EnumConstantDecl":({"pointer":22,"source_range":({"file":"/data/work/STAMP/bug_triage/tools/INFER-REGRESSION-TEST-BUFFER1-000009/minimal.c","line":8,"column":13},{"file":"/data/work/STAMP/bug_triage/tools/INFER-REGRESSION-TEST-BUFFER1-000009/minimal.c","line":8,"column":13})},{"name":"R","qual_name":["R","anonymous_enum_minimal.c:8:3","kwsincr"]},{"type_ptr":10},{})>],{},<"TTK_Enum">,{})>
```

From there, Infer is basically skipping this method.

If, however, we define this `enum {L, R}` with a `typedef`, it solves the problem:

```c
typedef enum {L, R} enumtype;

char *kwsincr()
{
register int depth;
enumtype dirs[12];


char arr[10];
if (depth < 10) {
/* POTENTIAL FLAW */
arr[10] = 1;
}

return 0;
}
```

With this version of the code, the bug is found and Infer does not complain about unimplemented features.

The source code leading to identification of this bug was created using Bug-Injector, see https://arxiv.org/abs/1901.02819.

贡献指南

打开贡献指南

评估

这个 Issue 还没有评估数据。

把新 issue 发到你的邮箱

精选适合新手参与的 GitHub issue 摘要。