facebook / facebook/infer

Infer issue with enum type

Ouverte
#1,094 2 commentaires 0 réactions 0 personnes assignées Voir sur GitHub
Langage dominant
OCaml
Étoiles
15.7k
Forks
2.1k
Merge moyen
19 h 36 min
PR mergées (30 j)
13

Description

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.

Guide de contribution

Ouvrir le guide de contribution

Évaluation

Cette issue n'a pas encore été évaluée.

Recevez les nouvelles issues par e-mail

Un résumé court des issues GitHub adaptées aux débutants.