Targeted Static Analysis for OCaml C Stubs - Eliminating Gremlins from the Code

Explore a conference talk on targeted static analysis for OCaml C stubs, focusing on eliminating errors in code. Learn about the challenges of writing OCaml user-defined primitives in C, including safety issues and lack of type checking. Discover how a new static analyzer can find known classes of bugs in C bindings, particularly useful for OCaml 5 migration. Examine the tool's functionality, which works with OCaml abstract parse and typed trees to generate header files and caller models. Understand how this analyzer, combined with a simplified OCaml runtime model, integrates with the Goblint static analysis framework to track and report incorrect dereferences of OCaml values. Gain insights into extending the analysis for additional safety properties and the potential for applying these tools and runtime models to other static analysis frameworks.

[OCaML'23] Targeted Static Analysis for OCaml C Stubs: Eliminating gremlins from the code