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

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

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