facebook / facebook/infer

Infer skips to analyze some files in a project with multiple mains?

Open
#1,153 1 comment 0 reactions 0 assignees View on GitHub
question
Dominant language
OCaml
Stars
15.7k
Forks
2.1k
Avg merge
19h 36m
Merged PRs (30d)
13

Description

- [x] Infer version I used: v0.15.0 (but I have the same issue with v0.17.0)
- [x] OS: Ubuntu 16.04

Hi.
I have a C project consists of multiple files with own mains, but Infer seems to analyze a single `main` procedure in specific file.
My Makefile is as below:
```
all: x.out y.out
x.out: x.o
gcc -o x.out x.o
y.out: y.o
gcc -o y.out y.o
x.o: x.c
gcc -c -o x.o x.c
y.o: y.c
gcc -c -o y.o y.c
```
`x.c` has two procedures `main` and `foo`, and `y.c` has `main` and `goo`.
I analyzed the project by the command `infer run -g --no-filtering -- make`, and got the following
results:
```
FF....
Found 2 issues

y.c:2: error: DEAD_STORE
The value written to &gy (type int) is never used.
1. void goo() {
2. > int gy = 2;
3. }
4.

y.c:6: error: DEAD_STORE
The value written to &y (type int) is never used.
4.
5. int main() {
6. > int y = 1;
7. goo_y();
8. }
```
The analysis log `FF....` says that Infer captured and analyzed two files and total 4 procedures (two mains, `foo` and `goo`), but I cannot find the analysis result both in the alarm report and `infer-out/specs`.
There are only 3 spec files in the directory: `foo.specs`, `goo.specs`, and `main.specs` (of `y.c`).

Is it intended? If so is there any way to get the spec of `main` in `x.c`?

Contributor guide

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.