Infer issue with enum type
- 主要语言
- 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 还没有评估数据。