Cannot detect call to function pointer inside a struct

[JukMR]

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

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.
• [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:

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:

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

Output of the command:

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

[dgutson]

Ping

[rgrig]

I was alerted about this issue by @hajduakos. I'll look into it this week.

[dgutson]

@rgrig thanks, it's basically when the functions are actually pointers inside a C structures. We couldn't find a way to specify a rule/pattern how to catch them.