facebook / facebook/infer

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

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

描述

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.

贡献指南

打开贡献指南

评估

这个 Issue 还没有评估数据。

把新 issue 发到你的邮箱

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