Support multi-threaded code

[nihilus]

I donnu if it is a know issue or not but IKOS fails pretty much to analyze posit threaded code regarding locking etc...

I understand that it might be out of the scope for the project, but it is so far the best open source static analyzer I've ever used so it's on my wish-list, however it might be more feasible to use dynamic analyzers like Valgrind for that.

[arthaud]

Hi @nihilus,

Yes, this is a known issue. IKOS doesn't handle multi-threaded code.

Handling multi-threaded code in a sound static analyzer based on Abstract Interpretation such as IKOS is challenging. There are a few research publications about this. Implementing it in IKOS would take some time.

This is unfortunately not a priority for us. I'm gonna keep this issue open for information and related questions.

[ivanperez-keera]

@arthaud this issue has been open for 4.5y and has seen no activity.

Why don't we just add a comment in TROUBLESHOOTING.md about the limitations analyzing multi-threaded code and close this issue?

[arthaud]

That's fine with me!

[ivanperez-keera]

I've just added a note at the end of the TROUBLESHOOTING.md document. Please see if this is enough or if you'd rather give more details (e.g., alternative approaches, limited analyses that do work, pointers to other tools).

If not, let me know and I'll merge.

Thanks!