Анализ значений для верхних границ петли

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, Харальд

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.

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