AutoFraming：基于 LLM 的 C 语言动态 Frame 规范合成方法

AutoFraming 是一种利用代码属性图引导 LLM 从 C 代码合成 ACSL frame 规范与功能契约的方法。在 84 个真实系统函数的测试中，该方法无错误 frame 规范成功率达 92.9%，比 SOTA 相对提升 179%，并在 51 函数测试集上达 96.1%。集成至现有 ACSL 合成框架后，其性能最高可提升 61.9%。