facebook / facebook/infer

Why can’t infer find some bugs in c code, such as uninitialized pointer variable, array accessed is out of bounds?

Aperta
#1,143 0 commenti 0 reazioni 0 assegnatari Vedi su GitHub
question
Lingua principale
OCaml
Stelle
15.7k
Fork
2.1k
Merge medio
19h 36m
PR unite (30g)
13

Descrizione

I am using infer version v0.17.0 . And I download the binary release "infer-linux64-v0.17.0.tar.xz" from this link : https://github.com/facebook/infer/releases/tag/v0.17.0. Linux version 16.04.10.

But I find that infer can't report some bugs, such as uninitialized pointer variable, array accessed is out of bounds. I delete the directory infer-out by rm -rf infer-out/ before runing infer command line every time.

****************************************************************************************************
Test 1:
test_1.c:
#include

int main()
{
int *p2;
*p2 = 20;

int array[5] = {3};
array[5] = 5;

int *p1 = NULL;
*p1 = 10;

return 0;
}

I run the command line " infer run -- gcc -c test_1.c"
result:
Capturing in make/cc mode...
Found 1 source file to analyze in /home/xwl/test/infer-out

Analysis finished in 140mss

No issues found

*****************************************************************************************
Test 2:
test_2.c:
#include

int main()
{
int *p1 = NULL;
*p1 = 10;

int *p2;
*p2 = 20;

int array[5] = {3};
array[5] = 5;

return 0;
}

I run the command line " infer run -- gcc -c test_2.c"
result:
Capturing in make/cc mode...
Found 1 source file to analyze in /home/xwl/test/infer-out

Analysis finished in 135mss

Found 1 issue

test.c:6: error: NULL_DEREFERENCE
pointer `p1` last assigned on line 5 could be null and is dereferenced at line 6, column 5.
4. {
5. int *p1 = NULL;
6. > *p1 = 10;
7.
8. int *p2;

Summary of the reports

NULL_DEREFERENCE: 1

**********************************************************************************************
Test 3:
test_3.c:
#include

int main()
{
int *p2;
*p2 = 20;

int array[5] = {3};
array[5] = 5;

return 0;
}

I run the command line " infer run -- gcc -c test_3.c"
result:
Capturing in make/cc mode...
Found 1 source file to analyze in /home/xwl/test/infer-out

Analysis finished in 139mss

No issues found

*************************************************************************************************
Test 4:
test_4.c:
#include

int main()
{
int array[5] = {3};
array[5] = 5;

return 0;
}

I run the command line " infer run -- gcc -c test_4.c"
result:
Capturing in make/cc mode...
Found 1 source file to analyze in /home/xwl/test/infer-out

Analysis finished in 146mss

No issues found

So I use infer in incorrect way, or infer really can't find the bugs.

Guida per i contributori

Apri la guida per i contributori

Valutazione

Questa issue non è ancora stata valutata.

Ricevi le nuove issue nella tua casella

Un breve riepilogo di issue GitHub adatte ai principianti.