Если несколько проверок выполнены на той же операции, Программа автоматического доказательства Кода выполняет их в определенном порядке. Порядок проверок важен, только если одна из проверок не является зеленой. Если проверка является красной, последующие проверки не выполнены. Если проверка является оранжевой, последующие проверки выполнены для уменьшаемого множества значений. Для получения дополнительной информации смотрите, что Анализ Программы автоматического доказательства Кода Следует за Красными и Оранжевыми Проверками.
Простым примером является порядок, начинает работу, указатель разыменовывают. Программа автоматического доказательства кода сначала проверяет, инициализируется ли указатель и затем проверяет, указывает ли указатель на допустимое местоположение. Проверка Illegally dereferenced pointer следует за проверкой Non-initialized local variable.
Если один из операндов в бинарной операции является переменной с плавающей точкой, Программа автоматического доказательства Кода выполняет эти проверки на операции в этом порядке:
Invalid operation on floats: Если вы позволяете опции рассмотреть неличные плавания, эта проверка определяет, может ли операция привести к NaN.
Overflow: Эта проверка определяет, переполняется ли результат.
Если вы позволяете опции рассмотреть неличные плавания, эта проверка определяет, может ли операция привести к бесконечностям.
Subnormal float: Если вы включаете субнормальный режим обнаружения, эта проверка определяет, может ли операция привести к субнормальным значениям.
Например, предположите, что вы позволяете опциям запретить бесконечности, NaNs и субнормальные результаты. В этом примере, операции y = x + 0; проверяется на все три проблемы. Операция кажется красной, но состоит из трех проверок: оранжевый Invalid operation on floats, оранжевый Overflow и красная проверка Subnormal float.
#include <float.h>
#include <assert.h>
double input();
int main() {
double x = input();
double y;
assert (x != x || x > DBL_MAX || (x > 0. && x < DBL_MIN));
y = x + 0.;
return 0;
}В + операция, x может иметь три группы значений: x NaN, x > DBL_MAX, и x > 0. && x < DBL_MIN.
Проверки выполнены в этом порядке:
Invalid operation on floats: проверка является оранжевой, потому что один путь к выполнению рассматривает тот x может быть NaN.
Для следующих проверок не рассматривается этот путь.
Overflow: проверка является оранжевой, потому что одна группа путей к выполнению рассматривает тот x > DBL_MAX. Для этой группы путей, + операция может привести к бесконечности.
Для следующей проверки не рассматривается эта группа путей.
Subnormal float: На остающейся группе путей к выполнению, x > 0. && x < DBL_MIN. Все значения x вызовите субнормальные результаты. Поэтому эта проверка является красной.
Сообщение на панели Result Details отражает это сокращение путей. Сообщение для проверки Subnormal float утверждает (when finite) показать, что бесконечные значения были удалены из фактора.
Значения для левых и правых операндов отражают все значения перед операцией, а не уменьшаемым множеством значений. Поэтому левый операнд все еще показывает Inf и NaN даже при том, что эти значения не были рассмотрены для проверки.
Consider non finite floats (-allow-non-finite-floats) | Infinities (-check-infinite) | Invalid operation on floats | NaNs (-check-nan) | Overflow | Subnormal float