Frama-c, недетерминированные значения с плавающей точкой

Question

В качестве примера я использую следующую функцию:

float nondet_float(){
  float x;
  return x;
}

int main(){
  float x = nondet_float();
  if(isnan(x)){
    some_error();
  }
}

Интересно, как мне использовать frama-c для симуляции недетерминированных операций с плавающей точкой?

Я хочу, чтобы переменная x рассматривалась как любое возможное значение с плавающей запятой, включая -inf, +inf и NaN.

Я хотел бы получить результат, что some_error() достижимо, если x равен NaN.

Итак, мой вопрос:

как мне симулировать недетерминированные поплавки? Как проверить доступность определенных вызовов функций?

Answer 1

Frama-C представляет собой набор плагинов, с разным уровнем поддержки для бесконечных /NaN значений с плавающей точкой. Я считаю, что WP поддерживает NaN и бесконечность; но это, вероятно, зависит от выбранной вами числовой модели (опция -wp-model).

Для плагина абстрактной интерпретации (EVA, ранее Value), NaN и бесконечности на данный момент не поддерживаются. Анализатор предполагает (и доказывает), что все значения с плавающей запятой конечны. Поддержка не конечных будет добавлена ​​в Frama-C Sulphur.

Кроме того, ваш nondet_float функция недействительна в любом случае. Возврат неинициализированных значений запрещен стандартом C, и эта функция будет помечена как неправильная, например, EVA. Вместо этого вы должны использовать функцию без тела, с предложением assigns \result \from \nothing как его спецификация.