facebook / infer

A static analyzer for Java, C, C++, and Objective-C
http://fbinfer.com/
MIT License
14.83k stars 2k forks source link

[Cpp] Biabduction seems not work #1702

Open skyleaworlder opened 1 year ago

skyleaworlder commented 1 year ago

Please make sure your issue is not addressed in the FAQ.

Please include the following information:

My code is the same as empty_vector_access:

#include <iostream>
#include <vector>

using namespace std;

int foo() {
  const std::vector<int> vec;
  return vec[0];
}

int main() {
  int elem = foo();
  return 0;
}

And my output is:

<summary>Click me</summary>
Found 1 source file to analyze in /home/lijg/selab/infer-sample-dataset/biabduction/empty_vector_access/cpp/infer-out
0/1 [................................................................................] 0% 54.246ms
|- [ 0.0s] idle
|- [ 0.0s] idle
|- [ 0.0s] idle
|- [ 0.0s] idle
|- [ 0.0s] idle
|- [ 0.0s] idle
|- [ 0.0s] idle
|- [ 0.0s] idle
|- [ 0.0s] idle
|- [ 0.0s] idle
0/1 [................................................................................] 0% 59.704ms
|- [ 0.0s] main.cpp: foo
|- [ 0.0s] idle
|- [ 0.0s] idle
|- [ 0.0s] idle
|- [ 0.0s] idle
|- [ 0.0s] idle
|- [ 0.0s] idle
|- [ 0.0s] idle
|- [ 0.0s] idle
|- [ 0.0s] idle
0/1 [................................................................................] 0% 84.284ms
|- [ 0.0s] main.cpp: main
|- [ 0.0s] idle
|- [ 0.0s] idle
|- [ 0.0s] idle
|- [ 0.0s] idle
|- [ 0.0s] idle
|- [ 0.0s] idle
|- [ 0.0s] idle
|- [ 0.0s] idle
|- [ 0.0s] idle
1/1 [################################################################################] 100% 86.928ms
|- [ 0.0s] idle
|- [ 0.0s] idle
|- [ 0.0s] idle
|- [ 0.0s] idle
|- [ 0.0s] idle
|- [ 0.0s] idle
|- [ 0.0s] idle
|- [ 0.0s] idle
|- [ 0.0s] idle
|- [ 0.0s] idle
1/1 [################################################################################] 100% 117ms
|- [ 0.0s] idle
|- [ 0.1s] idle
|- [ 0.1s] idle
|- [ 0.1s] idle
|- [ 0.1s] idle
|- [ 0.1s] idle
|- [ 0.1s] idle
|- [ 0.1s] idle
|- [ 0.1s] idle
|- [ 0.1s] idle
|- [ 0.1s] idle
No issues found  

In fact, not only empty_vector_access, dangling_pointer_dereference and some other issue types of biabductionare also not reported.