抽象诠释听起来像博士学位的要求。现在已经不是了
如何使用Infer在CI管道中运行形式化静态分析，包含可工作的配置和现实权衡。
抽象诠释是那种会让工程师关掉标签页的术语。它听起来像是需要花一学期格论才能理解的东西。大多数开发者都以为它活在研究论文里，而不是在拉取请求中。…
static-analysis
6 posts
LLM可以为你的静态分析警告排序。只是无法解释原因。
大语言模型可以帮助分流静态分析中的误报，但它们无法像抽象解释那样理解程序语义。以下是如何将两者结合。
你的静态分析器刚刚在一个周五下午发出了847条警告。从统计上看，其中大约5%到15%是真正的缺陷。其余都是误报：生成代码中的无效存储、对工具来说可疑但对人类来说显而易见的空值检查、无关紧要的哈希函数中的整数溢出。 手动逐一排查令人心力交瘁。于是你想：能不能直接问LLM哪些是真的？…
Meta用从不运行程序的静态分析器在投产代码中发现了10万个缺陷
Meta的Infer利用抽象解释和双向推理，通过推理代码结构而非执行来发现空指针解引用、内存泄漏和竞态条件。以下是它的工作原理以及如何在您自己的代码库中使用它。
Meta已经发布了超过10万个由静态分析器在代码到达用户之前捕获的缺陷修复。这个工具名为Infer，它是开源的，并且不会运行您的代码。它读取代码，构建代码可能执行的数学模型，并证明某些坏事不可能发生。或者它会找到一条可能发生的路径。…
静态分析无法证明你的飞机不会坠毁。但它能证明一些更有用的东西。
抽象解释会对每一种可能的程序状态进行过度近似。如果除零错误在抽象中不可达，那它在真实代码中就不可达。以下是它的工作原理以及它的局限性。
静态分析无法证明飞机不会坠毁。但它可以证明你的高度计控制回路永远不会出现除零运算、永远不会越界索引、永远不会使定点累加器溢出。这种区别很重要，因为前者是对物理、空气动力学和铝材在应力下的断言，而后者是对代码的断言——你可以在飞机离地之前就验证它。…
如何证明你的代码没有运行时错误（以及为什么你很可能会放弃尝试）
抽象解释让你在执行之前就证明运行时错误不可能发生。以下是它的实际工作原理、难点所在，以及它在你的工具链中的定位。
你的测试套件通过了。你的类型检查器全是绿色。你发布了。两小时后，生产环境在一个没人想到要测试的边界情况上抛出了 。 测试能发现 bug。类型系统能预防一部分。但两者都无法证明你的程序完全没有运行时错误。要做到这一点，你需要更强力的手段：一种能够同时对所有可能的执行路径进行推理、而无需实际运行代码的方法。…
Fuck-u-code：你的 AI 流水线遗忘的确定性质量关卡
你已经有类型检查、代码风格审查和架构规则。但你的确定性栈对复杂度、重复代码和命名灾难视而不见。以下是零成本的解决方案。
老实说，现在大多数 AI 代码流水线到底是什么样子。 你用 Cursor 或 Claude Code 生成代码。你运行 ，因为 TypeScript 严格模式能捕获类型不匹配。你运行 ESLint，因为没人想在合并请求里争论分号问题。也许你还会运行…