Migration to OCaml 5 requires updating a lot of C bindings due to the removal of naked pointer support. Writing OCaml user-defined primitives in C is a necessity, but is unsafe and error-prone. It does not benefit from either OCaml's or C's type checking, and existing C static analysers are not aware of the OCaml GC safety rules, and cannot infer them from existing macros alone.The alternative is automatically generating C stubs, which requires correctly managing value lifetimes. Having a static analyser for OCaml to C interfaces is useful outside the OCaml 5 porting effort too. After some motivating examples of real bugs in C bindings a static analyser is presented that finds these known classes of bugs. The tool works on the OCaml abstract parse and typed trees, and generates a header file and a caller model. Together with a simplified model of the OCaml runtime this is used as input to a static analysis framework, Goblint. An analysis is developed that tracks dereferences of OCaml values, and together with the existing framework reports incorrect dereferences. An example is shown how to extend the analysis to cover more safety properties. The tools and runtime models are generic and could be reused with other static analysis tools.

翻译：迁移到OCaml 5需要更新大量C绑定，因为裸指针支持已被移除。用C编写OCaml用户自定义原语虽属必要，但存在不安全且易出错的问题。这类代码既无法受益于OCaml或C的类型检查，而且现有的C静态分析器不了解OCaml垃圾回收安全规则，也无法仅从现有宏中推断这些规则。另一种方案是自动生成C存根，但这需要正确管理值的生命周期。拥有针对OCaml到C接口的静态分析器，在OCaml 5移植工作之外也同样有用。在列举C绑定中真实存在的若干典型错误示例后，本文提出一种能发现这些已知错误类型的静态分析器。该工具基于OCaml的抽象语法树和带类型标注的语法树工作，生成头文件和调用者模型。结合简化的OCaml运行时模型，将其作为输入提供给静态分析框架Goblint。通过开发一种追踪OCaml值解引用的分析方法，并结合现有框架报告非法的解引用操作。本文还展示了如何扩展该分析以覆盖更多安全属性。相关工具和运行时模型具有通用性，可与其他静态分析工具复用。