facebook / facebook/infer

Cannot detect call to function pointer inside a struct

Open
#1,712 4 comments 1 reaction 0 assignees View on GitHub
Dominant language
OCaml
Stars
15.7k
Forks
2.1k
Avg merge
19h 36m
Merged PRs (30d)
13

Description

Please make sure your issue is not addressed in the [FAQ](https://fbinfer.com/docs/support#troubleshooting).

Please include the following information:
- [x] The version of infer from `infer --version`.
- [x] Your operating system and version, for example "Debian 9", "MacOS High Sierra", whether you are using Docker, etc.
- [x] Which command you ran, for example `infer -- make`.
- [x] The full output in a paste, for instance a [gist](https://gist.github.com/).
- [x] If possible, a minimal example to reproduce your problem (for instance, some code where
infer reports incorrectly, together with the way you run infer to reproduce the incorrect
report).

* `Infer version v1.1.0-669338131`
* OS: `Linux 5.15.81-1-MANJARO`

Topl cannot detect the call to a function pointer located in a struct. Here is a simple example:

``` C
struct {
void (*func_to_void)(int arg1);
} *my_struct;

int main()
{
(my_struct->func_to_void) (1);

return 0;
}
```

I am particularly trying to detect the line `(my_struct->func_to_void) (1);` but without any success.

The property i'm using:

```
property anyName
start -> start: *
start -> error: ".*" (Arg1, VoidRet) when 1 == 1

property pointer
start -> start: *
start -> error: "\(->*\)" (Arg1, VoidRet) when 1 == 1

property fullname
start -> start: *
start -> error: "(my_struct->func_to_void)" (Arg1, VoidRet) when 1 == 1

property withoutParentesis
start -> start: *
start -> error: "my_struct->func_to_void" (Arg1, VoidRet) when 1 == 1

property somethingWithArrows
start -> start: *
start -> error: ".*->.*" (Arg1, VoidRet) when 1 == 1

property arrowExpansion
start -> start: *
start -> error: "\(\*my_struct\)\.func_to_void" (Arg1, VoidRet) when 1 == 1

```

I am running topl with:

``` bash
infer --topl-only --topl-properties simple_prop.topl --function-pointer-specialization -- clang -c -O0 simple_file.c
```

Output of the command:

```zsh
infer --topl-only --topl-properties simple_prop.topl --function-pointer-specialization -- clang -c -O0 simple_file.c
Capturing in make/cc mode...
Found 1 source file to analyze in /home/username/issue/infer-out
1/1 [################################################################################] 100% 46.852ms

No issues found

```

CC: @dgutson

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.