價值分析界定

我用下面的結構分析的控制程序：價值分析界定

unsigned int cnt=0; 
unsigned int inc=3; 
... 

void main(){ 
int i; 
int lim; 

for(i=0;i<100000;i++) 
{ 
    f1(); 
.... 
    lim = f2(); 
    if(cnt < lim) 
    cnt += inc; 
.... 
} 
}

我的目的是分析足夠的循環迭代表明CNT變量不能溢出。由於狀態空間會變得太高，單靠增加伸縮量將無濟於事。我看到，可以根據個人功能調整平板電腦。這也可以用於例如一個單一的if/else結構？對於這種環路結構，增加整個功能的平均值可能已經太多了。有沒有一種方法可以證明沒有寫入複雜的循環不變量和斷言而沒有溢出？

BR，哈拉爾

來源

2016-03-17 Harald

我已經採取了指定f2返回一些積極的自由。否則，測試if(cnt < lim)執行否定 - >無符號轉換，該值目前不能正確處理。而事實上，你的財產不是如果f2總是返回-1！

根據這個假設，cnt確實不是溢出。

unsigned int cnt=0; 
unsigned int inc=3; 

//@ assigns \result \from \nothing; ensures 0 <= \result; 
int f2(); 

void main(){ 
    int i; 
    int lim; 

    for(i=0;i<100000;i++) 
    { 
     f1(); 
     lim = f2();  
     if(cnt < lim) 
     cnt += inc; 
    } 
}

這是分析結果。 cnt還沒有溢出，因爲其最大值爲4294967295

[value] Values at end of function main: 
    cnt ∈ [0..2147483649],0%3 
    i ∈ {100000} 
    lim ∈ [0..2147483647]

如果f2可以返回負值< = -4，我不知道結果會不使用例如被證明WP插件。

關於你的問題的其餘部分，有很多方法可以更好地使用分析所需的時間量，但可能沒有什麼能夠幫助你。

來源

2016-03-17 20:28:00 byako

價值分析界定

回答

相關問題