數據流代碼路徑值範圍分析

我需要確定特定代碼行中變量的可能值範圍。在一個複雜的項目中，這可能非常乏味且容易出錯。這就是爲什麼我尋求一種可能性來自動執行此任務。想象一下以下簡單的代碼片段：數據流代碼路徑值範圍分析

#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 
}

是否有人知道的工具或爲一個完整的方式實現這一任務的任何其他方式嗎？此外，我想檢查結果值範圍對給定的一組值範圍，理想情況下只獲得不兼容的結果。

來源

2015-12-02 Philipp Michalski