AutoFraming：用 LLM 为 C 代码合成动态 frame 规约

AutoFraming 通过分析代码属性图（CPG）提取与 frame 相关的信息，引导 LLM 从 C 代码中合成 ACSL frame 规约。在 84 个来自真实系统的 ACSL 合规函数基准上，该方法为 92.9% 的函数生成了无错误的 frame 规约，相对当前最优技术提升 179%；在另一个 51 个函数的基准上，成功率从 80.4% 提升至 96.1%。