Infer results on Elina

[skcho]

Hello Gagan,

I tried running our analyzer Infer on Elina and got some signals. I report this because I thought you may be interested in addressing the signals and making Elina more stable. Full report is here.

       NULL_DEREFERENCE: 190
             DEAD_STORE: 127

• For NULL_DEREFERENCE, a lot of malloced pointers are used without null checks.
• For DEAD_STORE, I think most of them are legit.

  INFERBO_ALLOC_IS_ZERO: 67
      BUFFER_OVERRUN_L3: 46
      BUFFER_OVERRUN_S2: 16
            MEMORY_LEAK: 11
    UNINITIALIZED_VALUE: 9

• For the other signals, most of them are false positives, because the buffer overrun checker is under development (experimental) and Infer has not been focusing on C. I believe you can ignore them, though it may include true positives.

Sincerely,
Sungkeun

[skcho]

cc @mbouaziz

[GgnDpSngh]

Hi Sungkeun,

Thanks for your detailed feedback. I just quickly looked through the reported issues and agree that there might be DEAD_STORES. Regarding NULL_DEREFERENCES, currently, it is assumed that the call to malloc or calloc always succeeds as the analysis cannot proceed otherwise. This is done for enhancing performance as adding checks that always pass creates overhead. I will look into more detail if any of these can lead to a bug and let you know.

Cheers,
Gagan

[GgnDpSngh]

Hi Sungkeun,

I have fixed all dead stores except the few I think are not quite correctly reported by Infer. It seems that the majority of the stores were useful at some point but my text editor gedit could not detect when they became irrelevant. I will try to fix other signals reported by Infer soon.

Cheers,
Gagan

[skcho]

Hi Gagan,

Thank you for the fix. I was impressed that there are some cases where not simply removing a redundant store, but also fixing its semantics, e.g., changing type=res; to res=type;.

Note that the other type of signals, especially buffer overrun checker's INFERBO_ALLOC_IS_ZERO and BUFFER_OVERRUN_--, may include lots of false positives. Feel free to close this issue if you think it's done. :)

Sincerely,
Sungkeun

[GgnDpSngh]

Hi Sungkeun,

Indeed, that is why I will keep the issue around till I fix all issues reported by infer and inferbo as some may be genuine bugs.

Cheers,
Gagan