facebook / facebook/infer

Infer issue with enum type

Offen
#1,094 2 Kommentare 0 Reaktionen 0 zugewiesene Personen Auf GitHub ansehen
Vorherrschende Sprache
OCaml
Sterne
15.7k
Forks
2.1k
Ø Merge
19 Std. 36 Min.
Gemergte PRs (30 T.)
13

Beschreibung

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.

Beitragsleitfaden

Beitragsleitfaden öffnen

Bewertung

Dieses Issue wurde noch nicht bewertet.

Neue Issues direkt in Ihr Postfach

Eine kurze Übersicht über anfängerfreundliche GitHub-Issues.