c - 检测整数溢出的静态代码分析技术

Question

我正在尝试找到一些有效的技术，我可以将其作为我的整数溢出检测工具的基础。我知道有很多现成的检测工具，但我正在尝试自己实现一个简单的工具，这既是出于我个人对这一领域的兴趣，也是为了我的知识。

我知道诸如模式匹配和类型推断之类的技术，但我了解到需要更复杂的代码分析技术来检测 int 溢出。还有污点分析，它可以“标记”不受信任的数据源。

是否有其他一些我可能不知道的技术能够检测整数溢出？

Answer 1

也许值得尝试 cppcheck静态分析工具，即claims从版本 1.67 开始检测有符号整数溢出:

New checks:
- Detect shift by too many bits, signed integer overflow and dangerous sign conversion

请注意，它支持 C 和 C++ 语言。

对于无符号整数没有溢出检查，因为标准无符号类型永远不会溢出。

这是一些基本示例:

#include <stdio.h>

int main(void)
{
    int a = 2147483647;
    a = a + 1;

    printf("%d\n", a);

    return 0;
}

使用这样的代码，它得到:

$ ./cppcheck --platform=unix64 simple.c 
Checking simple.c...
[simple.c:6]: (error) Signed integer overflow for expression 'a+1'

但是我不会对它抱有太多期望(至少对于当前版本)，因为程序略有不同:

int a = 2147483647;
a++;

在没有注意到溢出的情况下通过。