Анализ диапазона значений пути кода потока данных

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 способен анализировать диапазоны значений, но является проприетарным решением.