数据流代码路径值范围分析

Question

我需要确定特定代码行中变量的可能值范围。在一个复杂的项目中，这可能是非常乏味和容易出错的。这就是为什么我寻求自动化这项任务的可能性。想象一下以下简单的代码片段：

#define checkBoundary(value) if((value)<100 || (value)> 1000) return;
bool checkmaximumForMode0(value)
{
    return (value>100);
}
void main(void)
{
    int mode = rand()%4;
    // x shall be any valid value for an int, just for the sake of completion i use rand here.
    int x = rand();
    if (x < 0) 
        return;
    switch(mode)
    {
    case 0:
        if(checkmaximumForMode0(x)) return;
    case 1: 
        checkBoundary(x);
    default:
        if (x<10000)
            goto exit;
    }
    // Now i want to know, which value range of x will i have under what circumstances
    int isChecked = x;
    // For this easy example:
    // Codepath 1(mode = 0): x >= 0 && x <= 100
    // Codepath 2(mode = 1): x >= 100 && x <= 1000
    // Codepath 3(mode = 2..3): x >= 10000 && x <= maxint
exit:
    print( "Exiting");
    return
}

有人知道一种工具或任何其他方法可以完整地完成这项任务吗？此外，我想对照给定的一组值范围来检查结果值范围，理想情况下只得到不兼容的结果。

Answer 1

我们目前正在使用clang静态分析器(http://clang-analyzer.llvm.org/)和cppcheck（它也适用于C）：http://cppcheck.sourceforge.net/

cppcheck（除了许多额外的检查之外）能够通过分析数据流来检查缓冲区的越界访问。另请参阅：http://sourceforge.net/p/cppcheck/wiki/ListOfChecks.

最后但同样重要的是，sonarqube附带了一些额外的检查（你必须为C/C++插件付费），并且能够在网页上显示所有内容。可以连接到Jenkins，也可以集成cppcheck结果和/或代码覆盖率：http://www.sonarqube.org

Answer 2

Polyspace能够分析价值范围，但它是一个专有的解决方案。