Значение анализа для высокой петли ограничивающая

Question

я анализирую программу управления со следующей структурой:

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, Harald

Answer 1

Я взял на себя смелость указать, что 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 плагин.

Что касается остальной части вашего вопроса, существуют различные альтернативы, позволяющие лучше использовать количество требуемого для анализа уровня расхода, но, вероятно, ничего не помогут вам здесь.