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的GC安全规则，无法仅从现有宏中推断出这些规则。另一种方法是自动生成C存根，这需要正确管理值生命周期。为OCaml到C接口提供静态分析器，在OCaml 5移植工作之外也很有价值。在列举了一些C绑定中真实错误的激励性示例后，本文提出了一种能发现这些已知错误类别的静态分析器。该工具基于OCaml的抽象解析树和类型化树，生成一个头文件和一个调用者模型。结合简化的OCaml运行时模型，这些内容被输入到静态分析框架Goblint中。我们开发了一种分析技术，用于追踪OCaml值的解引用，并结合现有框架报告不正确的解引用。本文还展示了如何扩展该分析以覆盖更多安全属性。这些工具和运行时模型是通用的，可与其他静态分析工具重复使用。